Transport, zeroth-order term, the Gårding inequality, and shifted existence #
We add to the principal part B_A of GeneralForm.lean a transport term bᵢ Dᵢu and a
zeroth-order term c u (both bounded measurable, c not assumed signed):
B[U, V] = ∑ᵢⱼ ⟪aᵢⱼ ∂ᵢu, ∂ⱼv⟫ + ∑ᵢ ⟪bᵢ ∂ᵢu, v₀⟫ + ⟪c u₀, v₀⟫.
This is Evans §6.1.1's full divergence-form operator Lu = -Dⱼ(aᵢⱼDᵢu) + bᵢDᵢu + cu.
- Gårding inequality (
FullEllipticOp.garding, Evans §6.2.2, Theorem 2(ii)): there areβ > 0,γ ≥ 0withβ ‖U‖²_{H¹} ≤ B[U, U] + γ ‖u₀‖²_{L²}for allU ∈ H₀¹(Ω). We takeβ = λ/2andγ = λ/2 + ‖c‖∞ + d ‖b‖∞² / (2λ). The transport term is absorbed into the ellipticity gap by the Peter-Paul (Young) inequality. - Shifted existence (
FullEllipticOp.weak_solution, Evans §6.2.2, Theorem 3): for any shiftμ ≥ γthe shifted formB_μ[U, V] = B[U, V] + μ ⟪u₀, v₀⟫is coercive (Gårding already controls the fullH¹norm, so no Poincaré inequality is needed here), and Lax-Milgram yields a unique weak solutionu ∈ H₀¹(Ω)ofLu + μu = ffor everyf ∈ H⁻¹(Ω).
The γ = 0 symmetric case (no transport, c ≥ 0, needing Poincaré) is the separate
EllipticCoeff.bilin_coercive of GeneralForm.lean.
Full divergence-form operator #
A full second-order divergence-form operator: a uniformly elliptic principal part A
together with a bounded measurable transport field b and zeroth-order coefficient c.
- b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ
Transport (first-order) coefficients.
- c : EuclideanSpace ℝ (Fin d) → ℝ
Zeroth-order coefficient.
- Bsup : ℝ
Sup bound on the transport field.
- Csup : ℝ
Sup bound on the zeroth-order coefficient.
The bound on the transport field is nonnegative.
The bound on the zeroth-order coefficient is nonnegative.
- b_meas (i : Fin d) : Measurable fun (x : EuclideanSpace ℝ (Fin d)) => self.b x i
Every component of the transport field is measurable.
- c_meas : Measurable self.c
The zeroth-order coefficient is measurable.
Every component of the transport field is bounded by
Bsupalmost everywhere.The zeroth-order coefficient is bounded by
Csupalmost everywhere.
Instances For
The transport coefficient bᵢ acting on L²(Ω).
Equations
- Op.bAct i = EllipticPdes.Sobolev.mulCoeffL ⋯ ⋯
Instances For
The zeroth-order coefficient c acting on L²(Ω).
Equations
- Op.cAct = EllipticPdes.Sobolev.mulCoeffL ⋯ ⋯
Instances For
Lower-order (transport + zeroth) bilinear form #
The lower-order part ∑ᵢ ⟪bᵢ ∂ᵢu, v₀⟫ + ⟪c u₀, v₀⟫ as a bare bilinear map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The lower-order bilinear form as a bounded form, with norm bound d·Bsup + Csup.
Equations
- Op.lowerBilin Ω = (Op.lowerBilinₗ Ω).mkContinuous₂ (↑d * Op.Bsup + Op.Csup) ⋯
Instances For
Simp lemma: unfolds lowerBilin Ω U V to the transport and zeroth-order inner products.
The full divergence-form bilinear form B = B_A + (transport + zeroth).
Equations
- Op.fullBilin Ω = Op.bilin Ω + Op.lowerBilin Ω
Instances For
fullBilin = B_A + lowerBilin: principal part plus transport and zeroth-order.
Gårding inequality #
The Gårding shift constant γ is non-negative.
Gårding inequality (Evans §6.2.2, Theorem 2(ii)). With β = λ/2 and γ the
shift constant, β ‖U‖²_{H¹} ≤ B[U, U] + γ ‖u₀‖²_{L²} for every U ∈ H₀¹(Ω).
Shifted coercivity and existence (Evans §6.2.2, Theorem 3) #
The zeroth L² form ⟪u₀, v₀⟫ on H₀¹(Ω), used for the spectral shift.
Equations
- EllipticPdes.Sobolev.FullEllipticOp.zerothForm Ω = (LinearMap.mk₂ ℝ (fun (U V : ↥(EllipticPdes.Sobolev.H01 Ω)) => inner ℝ ((↑U).ofLp 0) ((↑V).ofLp 0)) ⋯ ⋯ ⋯ ⋯).mkContinuous₂ 1 ⋯
Instances For
Simp lemma: zerothForm Ω U V = ⟪(U : H1amb Ω) 0, (V : H1amb Ω) 0⟫.
The shifted bilinear form B_μ[U, V] = B[U, V] + μ ⟪u₀, v₀⟫ associated to Lu + μu.
Equations
- Op.shiftedBilin Ω μ = Op.fullBilin Ω + μ • EllipticPdes.Sobolev.FullEllipticOp.zerothForm Ω
Instances For
Shifted coercivity (Evans §6.2.2, Theorem 3). For any shift μ ≥ γ, the shifted
form B_μ is
coercive with constant λ/2. The Gårding inequality already controls the full H¹ norm,
so no Poincaré inequality is needed.
Existence and uniqueness for Lu + μu = f (Evans §6.2.2, Theorem 3). For a
shift μ ≥ γ and
any continuous functional f on H₀¹(Ω), there is a unique u ∈ H₀¹(Ω) solving the shifted
weak problem B_μ[u, v] = f v for all v.
Transport-free, nonnegative-zeroth coercive case (Evans §6.2.2, closing #
Examples remark)
Nonnegativity of the lower-order form when the transport field vanishes (b = 0
a.e. on Ω) and the zeroth coefficient is nonnegative (c ≥ 0 a.e. on Ω): the
transport terms ⟪bᵢ ∂ᵢu, u₀⟫ are zero and ⟪c u₀, u₀⟫ = ∫_Ω c u₀² ≥ 0.
Quantitative coercivity for the transport-free, nonnegative-zeroth case
(Evans §6.2.2, closing Examples remark). If the transport field vanishes (b ≡ 0) and
the zeroth coefficient is
nonnegative (c ≥ 0), the full divergence form B = B_A + c dominates the full H¹
norm with the explicit constant λ / (C_P + 1): the zeroth term only helps, ellipticity
controls the gradient, and the Poincaré inequality lifts that to the full H¹ norm.
This is the constant-level form of [fullBilin_coercive_of_nonneg_zeroth]; the explicit
constant feeds the Lax-Milgram a-priori estimate.
Coercivity for the transport-free, nonnegative-zeroth case (Evans §6.2.2,
closing Examples remark). If the
transport field vanishes (b ≡ 0) and the zeroth coefficient is nonnegative (c ≥ 0), the
full divergence form B = B_A + c is coercive on H₀¹(Ω) without a spectral shift: the
zeroth term only helps, ellipticity controls the gradient, and the Poincaré inequality lifts
that to the full H¹ norm (the γ = 0 Gårding case, with constant λ / (C_P + 1)).
Existence and uniqueness for the transport-free, nonnegative-zeroth operator
(the γ = 0 specialisation of Evans's First Existence Theorem, §6.2.2). With b ≡ 0,
c ≥ 0, and the test-function Poincaré bound, the full
divergence form B = B_A + c is coercive with no spectral shift, so Lax-Milgram yields for
every continuous functional f on H₀¹(Ω) a unique weak solution u of Lu = f. This is
the existence theorem for Lu = -Dⱼ(aᵢⱼ Dᵢu) + cu with general uniformly elliptic A.
A-priori estimate for the weak solution (general uniformly elliptic operator,
b ≡ 0, c ≥ 0; the Lax-Milgram a-priori bound of Evans §6.2.1, Theorem 1). Under the
hypotheses of
[weak_solution_of_nonneg_zeroth], any weak solution obeys the Lax-Milgram estimate
‖u‖_{H₀¹} ≤ α⁻¹ ‖f‖ with the coercivity constant α = λ / (C_P + 1) of the form,
i.e. ‖u‖_{H₀¹} ≤ (C_P + 1) / λ · ‖f‖.
Unconditional existence, uniqueness, and a-priori bound on an open box, general
uniformly elliptic operator. The box specialisation of weak_solution_of_nonneg_zeroth:
on the coordinate box ∏ₖ (aₖ, bₖ), with b ≡ 0 and c ≥ 0, the test-function Poincaré
hypothesis is discharged from the box geometry. The per-direction slice bound
Poincare.slice_bound_euclBox (which rests on Poincare.poincare_box_dir) is averaged by
Poincare.poincare_testfn into the graph-coordinate bound with constant
C_P = C / (n + 1), so for every continuous functional f on H₀¹ of the box there is a
unique weak solution of Lu = -Dⱼ(aᵢⱼ Dᵢu) + cu = f, obeying the Lax-Milgram estimate
‖u‖_{H₀¹} ≤ α⁻¹ ‖f‖ with coercivity constant α = λ / (C / (n + 1) + 1), with no
abstract Poincaré input. This is Theorem thm: main with an H⁻¹ right-hand side; the
L² instance is [weak_solution_L2_of_nonneg_zeroth_euclBox].
Theorem thm: main: existence, uniqueness, and the a-priori bound on an open box,
L² right-hand side. For the general uniformly elliptic operator
Lu = -Dⱼ(aᵢⱼ Dᵢu) + cu with c ≥ 0 on the coordinate box ∏ₖ (aₖ, bₖ), and for every
f ∈ L²(Ω) entering through the pairing ⟨f, v⟩ = ∫_Ω f · v₀ (the embedding
L²(Ω) ⊆ H⁻¹(Ω), [l2Functional]), there is a unique weak solution u ∈ H₀¹(Ω) of
B[u, v] = ⟨f, v⟩, and every weak solution obeys ‖u‖_{H₀¹} ≤ α⁻¹ ‖f‖_{L²} with the
coercivity constant α = λ / (C / (n + 1) + 1) of the form. The Poincaré input is
discharged from the box geometry; no abstract hypothesis remains.
Existence, uniqueness, and the a-priori bound on any domain inside a coordinate
box, H⁻¹ right-hand side. For the uniformly elliptic operator
Lu = -Dⱼ(aᵢⱼ Dᵢu) + cu with c ≥ 0 on a domain Ω contained in the open box
∏ₖ (aₖ, bₖ), the test-function Poincaré hypothesis is discharged by
[Poincare.testfn_bound_of_subset_euclBox] from the geometry of the bounding box, with
side contributions (bᵢ - aᵢ)² / 2 ≤ C. Every continuous functional f on H₀¹(Ω)
admits a unique weak solution, obeying the Lax-Milgram estimate with coercivity
constant α = λ / (C / (n + 1) + 1). The L² instance is
[weak_solution_L2_of_nonneg_zeroth_of_subset_euclBox].
L² right-hand-side instance on any domain inside a coordinate box. For
f ∈ L²(Ω) entering through the pairing ⟨f, v⟩ = ∫_Ω f · v₀ ([l2Functional]), the
weak problem has a unique solution with ‖u‖_{H₀¹} ≤ α⁻¹ ‖f‖_{L²},
α = λ / (C / (n + 1) + 1). Derived from
[weak_solution_of_nonneg_zeroth_of_subset_euclBox].
Existence, uniqueness, and the a-priori bound on an arbitrary bounded domain,
L² right-hand side (Theorem thm: main in full generality). The Poincaré constant
CP is supplied by poincare_H01_of_bounded and is quantified before the datum, so it
depends only on Ω; every f ∈ L²(Ω) then obeys ‖u‖_{H₀¹} ≤ (CP + 1)/λ · ‖f‖_{L²}.
Terminal result of the library, stated in the manuscript. Nothing else consumes it.