TheoremStatement: 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.

Garding's inequality for a divergence-form elliptic operator

Statement

Assume Countable Choice (CC) (The Axiom of Countable Choice ( ${A C}_{ω}$ )) for the Sobolev and Lebesgue interfaces used by Uniformly elliptic divergence-form operators and their sesquilinear forms and The elliptic form is well defined and bounded on $H^{1}$ . Let $Ω \subseteq R^{n}$ be open, $n \geq 1$ , $K \in {R, C}$ , and let $L$ and its sesquilinear form $a$ be as in Uniformly elliptic divergence-form operators and their sesquilinear forms, with ellipticity constant $θ > 0$ and coefficient bounds $M_{a}, M_{b}, M_{c}$ . Then every $u \in H^{1} (Ω)$ satisfies $Re a (u, u) \geq \frac{θ}{2} ∥ D u ∥_{L^{2} (Ω)}^{2} - (\frac{n M_{b}^{2}}{2 θ} + M_{c}) ∥ u ∥_{L^{2} (Ω)}^{2},$ and consequently, with the explicit constants $α : = θ / 2$ and $β : = θ / 2 + n M_{b}^{2} / (2 θ) + M_{c}$ , $Re a (u, u) \geq α ∥ u ∥_{H^{1} (Ω)}^{2} - β ∥ u ∥_{L^{2} (Ω)}^{2} .$ Both inequalities restrict to $u \in H_{0}^{1} (Ω)$ . No Poincare inequality, no boundedness of $Ω$ and no symmetry of $a$ is used; the constants are explicit and are not claimed to be optimal.

Facts & Assumptions

Given: Countable Choice; an open set $Ω \subseteq R^{n}$ , $n \geq 1$ ; $K \in {R, C}$ ; a uniformly elliptic divergence-form operator $L$ and its form $a$ with ellipticity constant $θ > 0$ and coefficient bounds $M_{a}, M_{b}, M_{c}$ ; and $u \in H^{1} (Ω)$ (or $u \in H_{0}^{1} (Ω)$ ).

[F1]

Coefficients and form: $a^{i j}, b^{i}, c$ are measurable and essentially bounded with $∣ a^{i j} ∣ \leq M_{a}$ , $∣ b^{i} ∣ \leq M_{b}$ , $∣ c ∣ \leq M_{c}$ almost everywhere, the uniform ellipticity condition $Re (\sum_{i, j} a^{i j} (x) ξ_{j} \overline{ξ_{i}}) \geq θ ∣ ξ ∣^{2}$ holds for almost every $x$ and all $ξ \in C^{n}$ , and $a (u, u) = \int_{Ω} (a^{i j} D_{j} u \overline{D_{i} u} + b^{i} D_{i} u \overline{u} + c u \overline{u}) d x$ (Uniformly elliptic divergence-form operators and their sesquilinear forms, The essential supremum of a measurable function with respect to a measure, The space $L^{\infty} (μ)$ of essentially bounded measurable functions).

[F2]

The three integrals in [F1] are absolutely convergent for $u \in H^{1} (Ω)$ , so the real part of $a (u, u)$ is the sum of the real parts of the three integrals (The elliptic form is well defined and bounded on $H^{1}$ , Complex Lp classes and Euclidean test-function conventions).

[F3]

Holder and the coefficient bounds: for measurable functions with $∣ b^{i} ∣ \leq M_{b}$ , $∣ c ∣ \leq M_{c}$ almost everywhere, $∣ \int_{Ω} b^{i} D_{i} u \overline{u} d x ∣ \leq M_{b} ∥ D_{i} u ∥_{L^{2}} ∥ u ∥_{L^{2}}$ and $∣ \int_{Ω} c ∣ u ∣^{2} d x ∣ \leq M_{c} ∥ u ∥_{L^{2}}^{2}$ (Holder's inequality for integrals, including the endpoint cases, The space $L^{p} (μ)$ as the quotient by null functions).

[F4]

For real $r, s \geq 0$ and $θ > 0$ , Young's inequality with $p = q = 2$ gives $\sqrt{n} M_{b} r s \leq \frac{θ}{2} r^{2} + \frac{n M_{b}^{2}}{2 θ} s^{2}$ (Young's inequality for conjugate real exponents).

[F5]

Norm identity: on $H^{1} (Ω)$ and on its subspace $H_{0}^{1} (Ω)$ the norm satisfies $∥ u ∥_{H^{1}}^{2} = ∥ u ∥_{L^{2}}^{2} + ∥ D u ∥_{L^{2}}^{2}$ , where $∣ D u ∣^{2} = \sum_{i = 1}^{n} ∣ D_{i} u ∣^{2}$ (Integer-order Sobolev spaces and their norms, The notation $H^{k}$ and the reserved zero-boundary symbol, Zero-boundary Sobolev space as a norm closure).

[F6]

Finite-index Cauchy--Schwarz is Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs applied to $(∥ D_{i} u ∥_{2})_{i = 1}^{n}$ and $(1)_{i = 1}^{n}$ in Euclidean space. Elementary inequalities $∣ z ∣ \geq Re z$ and $∣ z ∣ \geq ∣ Re z ∣$ for complex $z$ , and $∥ D u ∥_{L^{2}}^{2} = \int_{Ω} ∣ D u ∣^{2}$ (Real and imaginary parts, complex conjugation, and modulus, Complex Lp classes and Euclidean test-function conventions).

Proof

technique · direct

1.1F1F6algebra

Principal part. Since $D u (x) \in C^{n}$ , applying the ellipticity hypothesis with $ξ = D u (x)$ gives $Re (a^{i j} (x) D_{j} u (x) \overline{D_{i} u (x)}) \geq θ ∣ D u (x) ∣^{2}$ for almost every $x \in Ω$ , and integration over $Ω$ yields $\int_{Ω} Re (a^{i j} D_{j} u \overline{D_{i} u}) d x \geq θ ∥ D u ∥_{L^{2}}^{2} .$

1.2F1F3F6algebra

Drift term. Pointwise $∣ b^{i} D_{i} u \overline{u} ∣ \leq M_{b} ∣ D_{i} u ∣ ∣ u ∣$ almost everywhere, so [F3] gives $∣ \int_{Ω} b^{i} D_{i} u \overline{u} d x ∣ \leq M_{b} ∥ D_{i} u ∥_{L^{2}} ∥ u ∥_{L^{2}}$ for each $i$ . Summing the $n$ terms and applying Cauchy--Schwarz in the index $i$ , $\sum_{i = 1}^{n} ∥ D_{i} u ∥_{L^{2}} \leq \sqrt{n} ∥ D u ∥_{L^{2}}$ , hence $∣ \int_{Ω} b^{i} D_{i} u \overline{u} d x ∣ \leq \sqrt{n} M_{b} ∥ D u ∥_{L^{2}} ∥ u ∥_{L^{2}},$ and in particular $Re \int_{Ω} b^{i} D_{i} u \overline{u} d x \geq - ∣ \int_{Ω} b^{i} D_{i} u \overline{u} d x ∣ \geq - \sqrt{n} M_{b} ∥ D u ∥_{L^{2}} ∥ u ∥_{L^{2}}$ .

1.3F1F3F6algebra

Reaction term. Since $∣ c u \overline{u} ∣ = ∣ c ∣ ∣ u ∣^{2} \leq M_{c} ∣ u ∣^{2}$ almost everywhere, [F3] gives $∣ \int_{Ω} c ∣ u ∣^{2} d x ∣ \leq M_{c} ∥ u ∥_{L^{2}}^{2}$ , so $Re \int_{Ω} c u \overline{u} d x \geq - M_{c} ∥ u ∥_{L^{2}}^{2}$ .

2.1F2step 1.1step 1.2step 1.3algebra

Combine the three terms. By [F2] the real part of $a (u, u)$ is the sum of the three real parts estimated in steps 1.1, 1.2 and 1.3: $Re a (u, u) \geq θ ∥ D u ∥_{L^{2}}^{2} - \sqrt{n} M_{b} ∥ D u ∥_{L^{2}} ∥ u ∥_{L^{2}} - M_{c} ∥ u ∥_{L^{2}}^{2} .$

3.1F4step 2.1algebra

Absorb the drift term. With $r = ∥ D u ∥_{L^{2}}$ and $s = ∥ u ∥_{L^{2}}$ , [F4] gives $\sqrt{n} M_{b} r s \leq \frac{θ}{2} r^{2} + \frac{n M_{b}^{2}}{2 θ} s^{2}$ , so step 2.1 yields the first displayed inequality $Re a (u, u) \geq \frac{θ}{2} ∥ D u ∥_{L^{2}}^{2} - (\frac{n M_{b}^{2}}{2 θ} + M_{c}) ∥ u ∥_{L^{2}}^{2} .$

4.1F5step 3.1givenalgebra∎

Replace the gradient norm using [F5]: $\frac{θ}{2} ∥ D u ∥_{L^{2}}^{2} = \frac{θ}{2} ∥ u ∥_{H^{1}}^{2} - \frac{θ}{2} ∥ u ∥_{L^{2}}^{2}$ , so the inequality of step 3.1 becomes $Re a (u, u) \geq α ∥ u ∥_{H^{1}}^{2} - β ∥ u ∥_{L^{2}}^{2}$ with $α = θ / 2$ and $β = θ / 2 + n M_{b}^{2} / (2 θ) + M_{c}$ ; both estimates descend to $u \in H_{0}^{1} (Ω)$ because $H_{0}^{1} (Ω) \subseteq H^{1} (Ω)$ and the norms agree, and no Poincare inequality, boundedness of $Ω$ or symmetry of $a$ entered any step.

Depends on

Used by

Dependency tree · two levels

67 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

John K. Hunter, Notes on Partial Differential Equations (UC Davis, revised 18 June 2014, complete 242-page notes) (standard reference, not scraped)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript, complete 392 pages) (standard reference, not scraped)
Leon Simon, Lectures on Partial Differential Equations (Stanford, complete 223-page author scan) (standard reference, not scraped)