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.

A sufficiently large shift is coercive

Statement

Assume Countable Choice. In the setting of Garding's inequality for a divergence-form elliptic operator put $a_{μ} (u, v) : = a (u, v) + μ (u, v)_{L^{2}}$ for $μ \in R$ . If $μ \geq β$ with $β : = θ / 2 + n M_{b}^{2} / (2 θ) + M_{c}$ , then $a_{μ}$ is a bounded sesquilinear form on $H^{1} (Ω)$ satisfying $Re a_{μ} (u, u) \geq \frac{θ}{2} ∥ u ∥_{H^{1} (Ω)}^{2} for every u \in H^{1} (Ω),$ and the same inequality holds for the restriction of $a_{μ}$ to $H_{0}^{1} (Ω)$ , so $a_{μ}$ is coercive with constant $θ / 2$ , independent of $μ$ once $μ \geq β$ (Bounded, coercive and symmetric sesquilinear forms). No boundedness of $Ω$ is used and the shift $μ$ is fixed.

Facts & Assumptions

Given: Countable Choice; an open set $Ω \subseteq R^{n}$ ; a uniformly elliptic operator $L$ and form $a$ with constants $θ, M_{a}, M_{b}, M_{c}$ ; a real $μ \geq β = θ / 2 + n M_{b}^{2} / (2 θ) + M_{c}$ ; and the form $a_{μ} = a + μ (\cdot, \cdot)_{L^{2}}$ .

[F1]

Garding's inequality: for every $u \in H^{1} (Ω)$ , $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 $Re a (u, u) \geq \frac{θ}{2} ∥ u ∥_{H^{1}}^{2} - β ∥ u ∥_{L^{2}}^{2}$ (Garding's inequality for a divergence-form elliptic operator).

[F2]

The form $a$ is sesquilinear on $H^{1} (Ω)$ and bounded: $∣ a (u, v) ∣ \leq (n M_{a} + n M_{b} + M_{c}) ∥ u ∥_{H^{1}} ∥ v ∥_{H^{1}}$ (The elliptic form is well defined and bounded on $H^{1}$ , Uniformly elliptic divergence-form operators and their sesquilinear forms).

[F3]

The $L^{2}$ pairing $(\cdot, \cdot)_{L^{2}}$ is sesquilinear and $∣ (u, v)_{L^{2}} ∣ \leq ∥ u ∥_{L^{2}} ∥ v ∥_{L^{2}} \leq ∥ u ∥_{H^{1}} ∥ v ∥_{H^{1}}$ , since on $H^{1}$ the norm satisfies $∥ w ∥_{H^{1}}^{2} = ∥ w ∥_{L^{2}}^{2} + ∥ D w ∥_{L^{2}}^{2}$ (Integer-order Sobolev spaces and their norms, The notation $H^{k}$ and the reserved zero-boundary symbol, Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs).

[F4]

$H^{1} (Ω)$ and its closed subspace $H_{0}^{1} (Ω)$ are Hilbert spaces for the Sobolev inner product (The Sobolev space $H^{1}$ is a Hilbert space). Coercivity on a Hilbert space means $Re a (u, u) \geq α ∥ u ∥^{2}$ with a constant $α > 0$ , and restriction of a form to the closed subspace $H_{0}^{1} (Ω) \subseteq H^{1} (Ω)$ preserves sesquilinearity and estimates (Bounded, coercive and symmetric sesquilinear forms, Zero-boundary Sobolev space as a norm closure).

Proof

technique · direct

1.1F2F3givenalgebra

Sesquilinearity and boundedness. The sum of the sesquilinear forms $a$ and $μ (\cdot, \cdot)_{L^{2}}$ is sesquilinear, and [F2] with [F3] gives for all $u, v \in H^{1} (Ω)$ $∣ a_{μ} (u, v) ∣ \leq ∣ a (u, v) ∣ + ∣ μ ∣ ∣ (u, v)_{L^{2}} ∣ \leq (n M_{a} + n M_{b} + M_{c} + ∣ μ ∣) ∥ u ∥_{H^{1}} ∥ v ∥_{H^{1}},$ so $a_{μ}$ is a bounded sesquilinear form on $H^{1} (Ω)$ .

1.2F1givenalgebra

Coercivity. For $u \in H^{1} (Ω)$ , $a_{μ} (u, u) = a (u, u) + μ ∥ u ∥_{L^{2}}^{2}$ has real part $Re a_{μ} (u, u) = Re a (u, u) + μ ∥ u ∥_{L^{2}}^{2} \geq \frac{θ}{2} ∥ u ∥_{H^{1}}^{2} - (β - μ) ∥ u ∥_{L^{2}}^{2} \geq \frac{θ}{2} ∥ u ∥_{H^{1}}^{2},$ by [F1] and $β - μ \leq 0$ . Hence $a_{μ}$ is coercive on $H^{1} (Ω)$ with constant $θ / 2$ .

2.1F4step 1.1step 1.2given∎

Restriction and conclusion. For $u \in H_{0}^{1} (Ω) \subseteq H^{1} (Ω)$ the same computation applies verbatim because the $H^{1}$ norm on the subspace is the restricted norm, so $a_{μ} ∣_{H_{0}^{1}}$ is bounded and satisfies $Re a_{μ} (u, u) \geq \frac{θ}{2} ∥ u ∥_{H^{1}}^{2}$ with the same constant $θ / 2$ ; the constant does not depend on $μ$ once $μ \geq β$ , and no boundedness of $Ω$ or Poincare inequality entered steps 1.1 and 1.2.

Depends on

Used by

Dependency tree · two levels

50 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)