LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge 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 sharp Dirichlet Poincare inequality on an interval

Statement

Assume Countable Choice. Let $L > 0$ , $I = (0, L)$ and $K \in {R, C}$ . Then every $u \in H_{0}^{1} (I; K)$ satisfies $∥ u ∥_{L^{2} (I)} \leq \frac{L}{π} ∥ u^{'} ∥_{L^{2} (I)} .$ The constant $L / π$ is optimal: $ϕ (x) = \sin (π x / L)$ belongs to $H_{0}^{1} (I)$ , is nonzero, and attains equality. Moreover $\int_{I} ϕ^{'} \overline{v^{'}} d x = (π / L)^{2} \int_{I} ϕ \overline{v} d x (v \in H_{0}^{1} (I)) .$ This is a direct interval inequality and weak identity; no spectral decomposition is assumed.

Facts & Assumptions

Given: Reals $L > 0$ and $k : = π / L$ , the interval $I = (0, L)$ , a field $K \in {R, C}$ , and the function $ϕ (x) : = \sin (k x)$ .

[F1]

$H_{0}^{1} (I; K) = W_{0}^{1, 2} (I; K)$ is the closure of $C_{c}^{\infty} (I; K)$ in the $W^{1, 2}$ norm, which for functions of one variable is $∥ v ∥_{H^{1}}^{2} = ∥ v ∥_{L^{2} (I)}^{2} + ∥ v^{'} ∥_{L^{2} (I)}^{2}$ ; complex test functions are defined by requiring both components to be real test functions, and the $L^{2}$ theory of complex classes is the componentwise one (Zero-boundary Sobolev space as a norm closure, Integer-order Sobolev spaces and their norms, Complex Lp classes and Euclidean test-function conventions).

[F2]

A classical smooth derivative on $I$ is the weak derivative of the class (Classical derivatives agree with weak derivatives). On a closed bounded interval a bounded Riemann integrable function is Lebesgue measurable and Lebesgue integrable with the same integral, a continuous function on $[a, b]$ is Riemann integrable, the Riemann integral is linear and additive over subintervals, and $m \leq h \leq M$ on $[a, b]$ gives $m (b - a) \leq \int_{a}^{b} h \leq M (b - a)$ (A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral, A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ , For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ , If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ ).

[F3]

Integration by parts and the second fundamental theorem on $[a, b]$ for differentiable functions with integrable derivatives (If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ , The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ).

[F4]

Trigonometric facts: $(\sin x)^{'} = \cos x$ , $(\cos x)^{'} = - \sin x$ , $\sin 0 = 0$ ; $\sin π = 0$ and $\sin x > 0$ for $0 < x < π$ ; $\sin^{2} x + \cos^{2} x = 1$ , $∣ \sin x ∣, ∣ \cos x ∣ \leq 1$ ; $∣ \sin u - \sin v ∣ \leq ∣ u - v ∣$ ; and the addition formulas, in particular $\cos 2 x = \cos^{2} x - \sin^{2} x$ and $\sin 2 π = 2 \sin π \cos π$ (The derivatives of sine and cosine are cosine and minus sine, Pi is the first positive zero of sine, Parity and the Pythagorean identity for sine and cosine, Sine and cosine are $1$ -Lipschitz on $R$ , The addition formulas for sine and cosine).

[F5]

Chain rule and the algebra of derivatives (sums, products, quotients away from zeros) for real functions (The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[F6]

The standard smooth step $σ$ is smooth with $σ (t) = 0$ for $t \leq 0$ and $σ (t) = 1$ for $t \geq 1$ ; hence $σ^{'} \equiv 0$ outside $(0, 1)$ and, being continuous on the compact interval $[0, 1]$ , the derivative satisfies $C_{σ} : = \sup_{R} ∣ σ^{'} ∣ < \infty$ (The standard smooth step function, Extreme value theorem: a continuous real function on a nonempty compact subset of $R$ attains a greatest and a least value).

[F7]

H"older's inequality and the quotient norms: for complex $L^{2}$ classes, $∣ \int f \overline{g} ∣ \leq ∥ f ∥_{2} ∥ g ∥_{2}$ , and the quotient norm obeys the triangle inequality, hence $∣ ∥ f ∥_{2} - ∥ g ∥_{2} ∣ \leq ∥ f - g ∥_{2}$ (Complex Holder, Minkowski, and the quotient norm).

[F8]

Countable Choice is assumed (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

1.1F4F5

Properties of $ϕ$ : differentiating $ϕ = \sin \circ (k i d)$ gives $ϕ^{'} (x) = k \cos (k x)$ and $ϕ^{''} (x) = - k^{2} \sin (k x) = - k^{2} ϕ (x)$ by the chain rule; $∣ ϕ^{'} ∣ \leq k$ because $∣ \cos ∣ \leq 1$ ; $ϕ > 0$ on $I$ because $0 < k x < π$ there; and the one-Lipschitz property of sine at the points $0$ , $k x$ and $π$ gives $∣ ϕ (x) ∣ = ∣ \sin (k x) - \sin 0 ∣ \leq k x$ and $∣ ϕ (x) ∣ = ∣ \sin (k x) - \sin π ∣ \leq k (L - x)$ for $x \in I$ .

1.2F2F3F4F5algebra

$ϕ$ is a nonzero class: $\sin^{2} t = \frac{1}{2} - \frac{1}{2} \cos 2 t$ and $\cos 2 t = 1 - 2 \sin^{2} t$ from the addition formulas and the Pythagorean identity give $ϕ^{2} = \frac{1}{2} - \frac{1}{2} \cos (2 k x)$ ; the antiderivative $x \mapsto \frac{\sin (2 k x)}{2 k}$ has derivative $\cos (2 k x)$ by the chain rule and vanishes at $x = 0$ and at $x = L$ , where $\sin (2 π) = 2 \sin π \cos π = 0$ . So $\int_{0}^{L} ϕ^{2} = \frac{L}{2} - \frac{1}{2} \int_{0}^{L} \cos (2 k x) d x = \frac{L}{2} > 0$ by linearity, the fundamental theorem and elementary bounds; in particular the $L^{2}$ class of $ϕ$ is not zero.

2.1F2F3F5step 1.1algebra

Real smooth case: let $a \in C_{c}^{\infty} (I; R)$ and put $w : = a / ϕ$ , a real $C_{c}^{\infty}$ function, since $supp a$ is a compact subset of $I$ on which $ϕ > 0$ . Then $a = ϕ w$ , so $a^{'} = ϕ^{'} w + ϕ w^{'}$ and $(∣ a^{'} ∣^{2} - k^{2} ∣ a ∣^{2}) = ϕ^{2} ∣ w^{'} ∣^{2} + (ϕ ϕ^{'} w^{2})^{'}$ : indeed $∣ a^{'} ∣^{2} = ϕ^{' 2} w^{2} + 2 ϕ ϕ^{'} w w^{'} + ϕ^{2} w^{' 2}$ while $(ϕ ϕ^{'} w^{2})^{'} = (ϕ^{' 2} + ϕ ϕ^{''}) w^{2} + 2 ϕ ϕ^{'} w w^{'} = (ϕ^{' 2} - k^{2} ϕ^{2}) w^{2} + 2 ϕ ϕ^{'} w w^{'}$ by step 1.1. Choose endpoints $r < s$ in $I$ with $supp a \subseteq (r, s)$ ; then $ϕ ϕ^{'} w^{2}$ vanishes at $r$ and $s$ , so the fundamental theorem gives $\int_{r}^{s} (ϕ ϕ^{'} w^{2})^{'} = 0$ and hence $\int_{I} (∣ a^{'} ∣^{2} - k^{2} ∣ a ∣^{2}) = \int_{I} ϕ^{2} ∣ w^{'} ∣^{2} \geq 0$ , all integrals agreeing in the Riemann and Lebesgue senses.

2.2F1F2F6F5step 1.1algebra

$ϕ \in H_{0}^{1} (I; K)$ : for integers $m \geq 4 / L$ put $η_{m} (x) : = σ (m x - 1) σ (m (L - x) - 1)$ and $ϕ_{m} : = η_{m} ϕ$ . Each factor is smooth, so $η_{m} \in C_{c}^{\infty} (I; R)$ with its support contained in $[1 / m, L - 1 / m] \subset I$ , hence $ϕ_{m} \in C_{c}^{\infty} (I; K)$ . By the chain and product rules, $η_{m}^{'} = (m σ^{'} (m x - 1)) σ (m (L - x) - 1) - σ (m x - 1) (m σ^{'} (m (L - x) - 1))$ , so $∣ η_{m}^{'} ∣ \leq 2 m C_{σ}$ , while $η_{m} = 1$ on $[2 / m, L - 2 / m]$ . Hence $ψ_{m} : = ϕ_{m} - ϕ$ is supported in $[0, 2 / m] \cup [L - 2 / m, L]$ , where $∣ ψ_{m} ∣ = ∣ (η_{m} - 1) ϕ ∣ \leq ∣ ϕ ∣ \leq 2 k / m$ by step 1.1, and $∣ ψ_{m}^{'} ∣ = ∣ η_{m}^{'} ϕ + (η_{m} - 1) ϕ^{'} ∣ \leq 2 m C_{σ} \cdot 2 k / m + k = 4 k C_{σ} + k$ there. So $∥ ψ_{m} ∥_{L^{2} (I)}^{2} \leq (2 k / m)^{2} L$ and, splitting the integral over the two strips, $∥ ψ_{m}^{'} ∥_{L^{2} (I)}^{2} \leq (4 k C_{σ} + k)^{2} \cdot 4 / m$ , both tending to $0$ . Thus $∥ ϕ_{m} - ϕ ∥_{H^{1}} \to 0$ with $ϕ_{m} \in C_{c}^{\infty} (I; K)$ , and $ϕ$ lies in the closure $H_{0}^{1} (I; K)$ .

2.3F2F3step 1.1

Weak identity on smooth tests: let $v \in C_{c}^{\infty} (I; K)$ and choose $a < b$ in $I$ with $supp v \subseteq (a, b)$ . Applying integration by parts to the real and imaginary parts of $v$ with the real function $ϕ^{'}$ gives $\int_{a}^{b} ϕ^{'} \overline{v^{'}} = [ϕ^{'} \overline{v}]_{a}^{b} - \int_{a}^{b} ϕ^{''} \overline{v} = k^{2} \int_{a}^{b} ϕ \overline{v}$ , since $ϕ^{'} v$ vanishes at $a$ and $b$ and $ϕ^{''} = - k^{2} ϕ$ by step 1.1.

3.1F1step 2.1algebra

Complex smooth case: let $u \in C_{c}^{\infty} (I; K)$ and write $u = a + i b$ with real $a, b \in C_{c}^{\infty} (I)$ (and $b = 0$ when $K = R$ ). Differentiation is componentwise, so $∣ u^{'} ∣^{2} = ∣ a^{'} ∣^{2} + ∣ b^{'} ∣^{2}$ and $∣ u ∣^{2} = a^{2} + b^{2}$ ; applying step 2.1 to $a$ and to $b$ and adding gives $\int_{I} (∣ u^{'} ∣^{2} - k^{2} ∣ u ∣^{2}) = \int_{I} ϕ^{2} (∣ w_{a}^{'} ∣^{2} + ∣ w_{b}^{'} ∣^{2}) \geq 0$ with $w_{a} = a / ϕ$ , $w_{b} = b / ϕ$ . Therefore every $u \in C_{c}^{\infty} (I; K)$ satisfies $∥ u ∥_{L^{2} (I)} \leq \frac{L}{π} ∥ u^{'} ∥_{L^{2} (I)}$ , since $k = π / L$ .

3.2F1F7step 2.3

Weak identity on $H_{0}^{1}$ : define $Λ (v) : = \int_{I} ϕ^{'} \overline{v^{'}} - k^{2} \int_{I} ϕ \overline{v}$ for $v \in H_{0}^{1} (I; K)$ . By H"older, $∣ Λ (v) ∣ \leq (∥ ϕ^{'} ∥_{2} + k^{2} ∥ ϕ ∥_{2}) ∥ v ∥_{H^{1}}$ , so $Λ$ is bounded, and it vanishes on $C_{c}^{\infty} (I; K)$ by step 2.3. For arbitrary $v \in H_{0}^{1}$ take $v_{n} \in C_{c}^{\infty} (I; K)$ with $∥ v_{n} - v ∥_{H^{1}} \to 0$ ; then $∣ Λ (v) ∣ = ∣ Λ (v) - Λ (v_{n}) ∣ \leq C ∥ v - v_{n} ∥_{H^{1}} \to 0$ , so $Λ (v) = 0$ . Hence $\int_{I} ϕ^{'} \overline{v^{'}} = k^{2} \int_{I} ϕ \overline{v}$ for every $v \in H_{0}^{1} (I; K)$ .

4.1F1F7F8step 3.1

Approximation: let $u \in H_{0}^{1} (I; K)$ . By definition of the closure there are $u_{n} \in C_{c}^{\infty} (I; K)$ with $∥ u_{n} - u ∥_{H^{1}} \to 0$ , so $∥ u_{n} - u ∥_{L^{2}} \to 0$ and $∥ u_{n}^{'} - u^{'} ∥_{L^{2}} \to 0$ . Step 3.1 gives $∥ u_{n} ∥_{2} \leq \frac{L}{π} ∥ u_{n}^{'} ∥_{2}$ for every $n$ , and the reverse triangle inequality turns both sides into convergent sequences with limits $∥ u ∥_{2}$ and $∥ u^{'} ∥_{2}$ ; passing to the limit gives $∥ u ∥_{L^{2} (I)} \leq \frac{L}{π} ∥ u^{'} ∥_{L^{2} (I)}$ .

5.1step 2.2step 1.2step 3.2algebra∎

Optimality: step 2.2 puts $ϕ$ in $H_{0}^{1} (I; K)$ and step 1.2 makes it nonzero; taking $v = ϕ$ in the identity of step 3.2 gives $∥ ϕ^{'} ∥_{L^{2}}^{2} = k^{2} ∥ ϕ ∥_{L^{2}}^{2}$ , that is $∥ ϕ ∥_{L^{2}} = \frac{L}{π} ∥ ϕ^{'} ∥_{L^{2}}$ : the constant $L / π$ is attained, hence optimal.

Depends on

Used by

The Dirichlet Laplacian generates an analytic heat semigroup Corollary
A large adverse zero-order term destroys Dirichlet coercivity Counterexample
L² forcing defines an H⁻¹ functional Example
The Rayleigh quotient on an interval Example

Dependency tree · two levels

122 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

Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (2011) (standard reference, not scraped)