CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Poincare constant is the reciprocal square root of the first Dirichlet eigenvalue

Statement

Assume the Axiom of Choice and Countable Choice. Let $Ω \subseteq R^{n}$ be nonempty bounded open and consider the Dirichlet Laplacian, i.e. the symmetric case with $a^{i j} = δ^{i j}$ , $b = 0$ , $c = 0$ (Uniformly elliptic divergence-form operators and their sesquilinear forms). Then its first eigenvalue satisfies $λ_{1} > 0$ and $λ_{1} = \min_{u \in H_{0}^{1} (Ω) ∖ {0}} \frac{∥ D u ∥_{L^{2}}^{2}}{∥ u ∥_{L^{2}}^{2}}, ∥ u ∥_{L^{2} (Ω)} \leq λ_{1}^{- 1 / 2} ∥ D u ∥_{L^{2} (Ω)} (u \in H_{0}^{1} (Ω)),$ with equality for nonzero $u$ exactly at the nonzero first eigenfunctions; $u = 0$ is also the trivial equality case. Hence $λ_{1}^{- 1 / 2}$ is the optimal (smallest) constant in the $L^{2}$ zero-trace Poincare inequality on $Ω$ : every constant $C$ with $∥ u ∥_{L^{2}} \leq C ∥ D u ∥_{L^{2}}$ for all $u \in H_{0}^{1} (Ω)$ satisfies $C \geq λ_{1}^{- 1 / 2}$ , and the positive admissible constant $C_{P}$ of The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction at $p = 2$ therefore satisfies $C_{P} \geq λ_{1}^{- 1 / 2}$ . No numerical value or domain formula for $λ_{1}$ is asserted.

Facts & Assumptions

Given: the Axiom of Choice and Countable Choice; a nonempty bounded open set $Ω \subseteq R^{n}$ ; the Dirichlet Laplacian form $a (u, v) = \int_{Ω} D u \cdot \overline{D v} d x$ on $H_{0}^{1} (Ω)$ with eigenvalues $λ_{j}$ and eigenbasis ${e_{j}}$ .

[F1]

Rayleigh principle: for the symmetric case, $λ_{1} = \min_{u \neq 0} a (u, u) / ∥ u ∥_{L^{2}}^{2}$ , attained exactly on the nonzero elements of the first eigenspace, and $λ_{1}$ is the smallest weak eigenvalue; for the Dirichlet Laplacian $a (u, u) = ∥ D u ∥_{L^{2}}^{2}$ (The Rayleigh principle for the first Dirichlet eigenvalue, The $L^{2}$ operator associated with a symmetric elliptic form, Discrete spectrum of a symmetric elliptic Dirichlet operator, Uniformly elliptic divergence-form operators and their sesquilinear forms).

[F2]

Since $Ω$ is bounded, it lies in a finite-width slab. The supplier at $p = 2$ gives a finite Poincare constant for every $u \in W_{0}^{1, 2} (Ω; C) = H_{0}^{1} (Ω)$ ; enlarge it if necessary and fix a positive admissible $C_{P}$ , so $∥ u ∥_{L^{2} (Ω)} \leq C_{P} ∥ D u ∥_{L^{2} (Ω)}$ (The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction, Zero-boundary Sobolev space as a norm closure, Integer-order Sobolev spaces and their norms, The space $L^{p} (μ)$ as the quotient by null functions, The Axiom of Choice).

Proof

technique · direct

1.1F1F2givenalgebra

Positivity and the minimum. With $a (u, u) = ∥ D u ∥_{L^{2}}^{2}$ , the Rayleigh principle [F1] identifies $λ_{1}$ with the displayed minimum, attained exactly on the nonzero first eigenfunctions. Fix the positive admissible $C_{P}$ of [F2]. For every $u \neq 0$ , Poincare gives $∥ D u ∥_{L^{2}}^{2} / ∥ u ∥_{L^{2}}^{2} \geq C_{P}^{- 2} > 0$ , so $λ_{1} \geq C_{P}^{- 2} > 0$ .

2.1F1step 1.1givenalgebra

The inequality and its equality cases. For nonzero $u \in H_{0}^{1} (Ω)$ , the identity $λ_{1} = \min_{v \neq 0} ∥ D v ∥^{2} / ∥ v ∥^{2}$ gives $∥ D u ∥_{L^{2}}^{2} \geq λ_{1} ∥ u ∥_{L^{2}}^{2}$ , hence $∥ u ∥_{L^{2}} \leq λ_{1}^{- 1 / 2} ∥ D u ∥_{L^{2}}$ . Equality for nonzero $u$ holds exactly when its Rayleigh quotient equals $λ_{1}$ , which by [F1] is exactly at the nonzero first eigenfunctions. At $u = 0$ both sides are zero.

3.1F2step 2.1givenalgebra∎

Optimality. Let $C$ be any constant with $∥ u ∥_{L^{2}} \leq C ∥ D u ∥_{L^{2}}$ for all $u \in H_{0}^{1} (Ω)$ . Testing at a nonzero first eigenfunction $e_{1}$ , step 2.1 gives $∥ e_{1} ∥_{L^{2}} = λ_{1}^{- 1 / 2} ∥ D e_{1} ∥_{L^{2}} \leq C ∥ D e_{1} ∥_{L^{2}}$ . Moreover $∥ D e_{1} ∥_{L^{2}} > 0$ : if it were zero, [F2] would imply $∥ e_{1} ∥_{L^{2}} \leq C_{P} ∥ D e_{1} ∥_{L^{2}} = 0$ , contradicting $e_{1} \neq 0$ . Thus $C \geq λ_{1}^{- 1 / 2}$ . Hence $λ_{1}^{- 1 / 2}$ is the smallest admissible constant, and the particular constant $C_{P}$ of the zero-trace Poincare inequality satisfies $C_{P} \geq λ_{1}^{- 1 / 2}$ .

Depends on

Used by

The Dirichlet Laplacian generates an analytic heat semigroup Corollary
The analytic Dirichlet heat semigroup Example

Dependency tree · two levels

56 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Richard S. Laugesen, Spectral Theory of Partial Differential Equations (University of Illinois lecture notes, arXiv:1203.2344, complete 120 pages) (standard reference, not scraped)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript, complete 392 pages) (standard reference, not scraped)
John K. Hunter, Notes on Partial Differential Equations (UC Davis, revised 18 June 2014, complete 242-page notes) (standard reference, not scraped)