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

A positive reaction term restores coercivity without Poincar'e

Statement

Assume Countable Choice. Let $Ω \subseteq R^{n}$ be open (no boundedness and no Dirichlet boundary condition assumed), and let $a$ be the divergence form of Uniformly elliptic divergence-form operators and their sesquilinear forms on $H^{1} (Ω)$ with ellipticity constant $θ$ , coefficient bounds $M_{a}, M_{b}, M_{c}$ where $∣ b^{i} ∣ \leq M_{b}$ componentwise, and ${ess inf}_{Ω} Re c \geq c_{0} > 0, \sqrt{n} M_{b} < 2 \min (θ, c_{0}) .$ Then $a$ is coercive on $Ω$ with constant $α : = \min (θ, c_{0}) - \sqrt{n} M_{b} / 2 > 0$ : $Re a (u, u) \geq α ∥ u ∥_{H^{1} (Ω)}^{2} (u \in H^{1} (Ω)) .$ Consequently The Lax--Milgram theorem applies on the Hilbert space $H^{1} (Ω)$ and gives, for every bounded conjugate-linear functional $F$ on $H^{1} (Ω)$ , a unique $u \in H^{1} (Ω)$ with $a (u, v) = F (v)$ for all $v$ : a second legitimate coercivity mechanism, driven by the reaction coefficient rather than by a Poincar'e inequality or boundary condition. When $b \equiv 0$ , taking $M_{b} = 0$ , the condition is $ess inf Re c > 0$ only.

Facts & Assumptions

Given: Countable Choice; an open $Ω \subseteq R^{n}$ ; divergence-form coefficients $a^{i j}, b^{i}, c$ with bounds $M_{a}, M_{b}, M_{c}$ , where $∣ b^{i} ∣ \leq M_{b}$ componentwise, and ellipticity constant $θ > 0$ ; ${ess inf}_{Ω} Re c \geq c_{0} > 0$ ; the assumption $\sqrt{n} M_{b} < 2 \min (θ, c_{0})$ ; and $α : = \min (θ, c_{0}) - \sqrt{n} M_{b} / 2 > 0$ .

[F1]

Uniform ellipticity gives for a.e. $x$ and $ξ = D u (x)$ : $Re (a^{i j} D_{j} u \overline{D_{i} u}) \geq θ ∣ D u ∣^{2}$ ; the coefficient bounds give $∣ b^{i} ∣ \leq M_{b}$ and $∣ c ∣ \leq M_{c}$ a.e. (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 form $a$ is bounded on $H^{1} (Ω)$ by The elliptic form is well defined and bounded on $H^{1}$ , and $H^{1} (Ω)$ is a Hilbert space (The Sobolev space $H^{1}$ is a Hilbert space, Integer-order Sobolev spaces and their norms).

[F3]

Estimates: $Re \int_{Ω} c u \overline{u} d x = \int_{Ω} (Re c) ∣ u ∣^{2} d x \geq c_{0} ∥ u ∥_{L^{2}}^{2}$ ; componentwise $∣ b^{i} ∣ \leq M_{b}$ and $\sum_{i} ∣ D_{i} u ∣ \leq \sqrt{n} ∣ D u ∣$ imply $∣ \int_{Ω} b^{i} D_{i} u \overline{u} d x ∣ \leq \sqrt{n} M_{b} ∥ D u ∥_{L^{2}} ∥ u ∥_{L^{2}}$ by pointwise Cauchy--Schwarz and H"older; also $2 a b \leq a^{2} + b^{2}$ for nonnegative reals (Holder's inequality for integrals, including the endpoint cases, Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation, Real and imaginary parts, complex conjugation, and modulus).

[F4]

Lax--Milgram applies to bounded coercive forms on Hilbert spaces (The Lax--Milgram theorem, Bounded, coercive and symmetric sesquilinear forms).

Proof

1.1F1F2

Pointwise decomposition and integration: by [F1], for almost every $x$ the principal integrand satisfies $Re (a^{i j} D_{j} u \overline{D_{i} u}) \geq θ ∣ D u (x) ∣^{2}$ , and integrating (the principal term is absolutely convergent by [F2]) gives $Re \int_{Ω} a^{i j} D_{j} u \overline{D_{i} u} d x \geq θ ∥ D u ∥_{L^{2}}^{2} .$

2.1F1F3step 1.1algebra

Drift and reaction terms: taking real parts of the definition of $a$ , $Re a (u, u) \geq θ ∥ D u ∥_{L^{2}}^{2} - \sqrt{n} M_{b} ∥ D u ∥_{L^{2}} ∥ u ∥_{L^{2}} + c_{0} ∥ u ∥_{L^{2}}^{2},$ where the drift term is bounded in absolute value by $\sqrt{n} M_{b} ∥ D u ∥_{L^{2}} ∥ u ∥_{L^{2}}$ via [F3], and the reaction term is bounded below by $c_{0} ∥ u ∥_{L^{2}}^{2}$ using $Re c \geq c_{0}$ a.e.

3.1F3step 2.1algebra

Coercivity: applying $2 a b \leq a^{2} + b^{2}$ to $a = ∥ D u ∥_{L^{2}}$ , $b = ∥ u ∥_{L^{2}}$ with weight $\sqrt{n} M_{b}$ gives $\sqrt{n} M_{b} ∥ D u ∥ ∥ u ∥ \leq \frac{\sqrt{n} M_{b}}{2} (∥ D u ∥_{L^{2}}^{2} + ∥ u ∥_{L^{2}}^{2})$ , hence $Re a (u, u) \geq (θ - \frac{\sqrt{n} M_{b}}{2}) ∥ D u ∥_{L^{2}}^{2} + (c_{0} - \frac{\sqrt{n} M_{b}}{2}) ∥ u ∥_{L^{2}}^{2} \geq α ∥ u ∥_{H^{1} (Ω)}^{2}$ with $α = \min (θ, c_{0}) - \frac{\sqrt{n} M_{b}}{2} > 0$ , because $∥ u ∥_{H^{1}}^{2} = ∥ u ∥_{L^{2}}^{2} + ∥ D u ∥_{L^{2}}^{2}$ and both coefficients $θ - \frac{\sqrt{n} M_{b}}{2}$ , $c_{0} - \frac{\sqrt{n} M_{b}}{2}$ are at least $α$ by the smallness hypothesis.

4.1F2F4step 3.1∎

Consequences: $a$ is bounded by [F2] and coercive with constant $α$ by step 3.1, so Lax--Milgram applies on the Hilbert space $H^{1} (Ω)$ : for every bounded conjugate-linear functional $F$ there is a unique $u \in H^{1} (Ω)$ with $a (u, v) = F (v)$ for all $v$ . No Poincar'e inequality, boundary condition or integration by parts was used; when $b \equiv 0$ , taking $M_{b} = 0$ , the hypothesis reduces to $ess inf Re c > 0$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

72 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 two-quarter notes) (standard reference, not scraped)
Leon Simon, Lectures on Partial Differential Equations (Stanford, complete 223-page author scan) (standard reference, not scraped)
Richard S. Laugesen, Linear Analysis and Partial Differential Equations (University of Illinois, 2020, complete 158-page graduate notes) (standard reference, not scraped)