The divergence-form energy form on H¹(Ω), and Gårding's inequality #
Lane D, item 16 of TauCetiRoadmap/PDE/README.md asks for the weak energy form
a(u, v) = ∫_Ω aⁱʲ ∂ᵢu ∂ⱼv + bⁱ ∂ᵢu v + c u v
of a divergence-form operator L u = -∂ⱼ(aⁱʲ ∂ᵢu) + bⁱ ∂ᵢu + c u, together with Gårding's
inequality a(u, u) ≥ α‖u‖²_{H¹} - β‖u‖²_{L²} and the lower bounds used to establish
coercivity on H¹₀(Ω) under suitable hypotheses. The pointwise and raw-jet halves of that
program are already in place: TauCeti.PDE.energyIntegrand is the
pointwise jet form and TauCeti.PDE.energyFormIntegral its integral against a measure, stated
for raw jet fields X → ℝ × EuclideanSpace ℝ ι because the Sobolev space was a separate
prerequisite. That prerequisite is now TauCeti.W1p, and this file joins the two.
The energy form on Sobolev functions #
TauCeti.PDE.jetField u is the raw value-gradient jet field x ↦ (u x, ∇u x) of a Sobolev
function, and TauCeti.PDE.energyFormH1 a b c u v integrates the pointwise energy density
against it. Both components of the jet are L² on Ω, so the energy density of two Sobolev
functions is integrable as soon as their pointwise bilinear form is essentially bounded
(TauCeti.PDE.integrable_energyIntegrand_jetField). The bounds-based wrapper
TauCeti.PDE.UniformlyEllipticOn.integrable_energyIntegrand_jetField constructs that hypothesis
from measurable bounded coefficients.
Gårding, and what coercivity needs #
The pointwise Gårding bound absorbs the drift by Young's inequality, paying for it out of half of the ellipticity floor, and integrating it gives
a(u, u) ≥ (λ/2)‖∇u‖²_{L²} - (β²/2λ)‖u‖²_{L²}
for every u ∈ H¹(Ω), with λ the lower ellipticity constant, β a bound for the drift and
c ≥ 0 (TauCeti.PDE.UniformlyEllipticOn.garding_energyFormH1_self). This is not yet
coercivity, and under the hypotheses assumed here the negative L² term cannot be dropped:
c ≥ 0 allows c = 0, and then on a domain of finite measure a nonzero constant lies in
H¹(Ω) with zero gradient, so no lower bound by a positive multiple of ‖u‖²_{H¹} holds. It
is the weakness of c ≥ 0 that is responsible, not H¹(Ω) itself: a mass coefficient bounded
below by a constant δ satisfying β² < 4λδ controls constants too. A positive Young
parameter ε between β²/(4δ) and λ makes both coefficients in
TauCeti.PDE.UniformlyEllipticOn.garding_energyFormH1_self_of_mass_lower_bound_with_parameter
positive.
A Poincaré inequality ‖u‖_{L²} ≤ P‖∇u‖_{L²} closes the gap, and
TauCeti.W1p.norm_value_le_mul_norm_gradient_of_subset_slab supplies one on H¹₀(Ω) for a
domain trapped in a slab. The resulting bound
a(u, u) ≥ (λ² - β²P²)/(2λ(P² + 1)) · ‖u‖²_{H¹}
holds outright (TauCeti.PDE.UniformlyEllipticOn.mul_norm_sq_le_energyFormH1_self_of_poincare),
and it is coercivity once its constant is positive, for which
TauCeti.PDE.energyFormH1_poincare_constant_pos
supplies the sufficient smallness condition βP < λ relating the drift to the ellipticity and
the domain; with no drift there is no smallness condition at all. The
condition is what this estimate needs, not a proof that coercivity fails without it; when
coercivity is genuinely unavailable, the Fredholm alternative (Lane D, item 18) takes the place
of Lax--Milgram.
Boundedness is the other half of the pair the energy method needs, and it comes from the
pointwise operator-norm bound Λ + β + γ on the energy integrand together with Cauchy--Schwarz
(TauCeti.PDE.UniformlyEllipticOn.norm_energyFormH1_le). Bilinearity and that bound package the
form as a bundled continuous bilinear map on H¹(Ω)
(TauCeti.PDE.energyFormH1L), by restricting the existing
TauCeti.PDE.energyFormLpVariable along the Sobolev jet inclusion. Restricting further along the
closed-subspace inclusion gives TauCeti.PDE.energyFormH1L0 on H¹₀(Ω). These forms have the
shape required by Lax--Milgram. The Poincaré route gives coercivity on H¹₀(Ω) when βP < λ.
The mass condition β² < 4λδ instead gives coercivity on all of H¹(Ω), with explicit
constant min (λ - ε) (δ - β²/(4ε)) for a suitable ε, independently of the domain. This file
supplies both lower bounds and does not package an IsCoercive proof; that packaging is
TauCeti.PDE.isCoercive_energyFormH1L0 in TauCeti/Analysis/PDE/DirichletProblem.lean.
Everything is stated with explicit constants λ, Λ, β, γ, P, as the roadmap's standing
hypotheses require, and coefficient bounds are inline hypotheses ∀ x ∈ Ω, ‖b x‖ ≤ β rather
than a bespoke predicate. No boundary regularity of Ω is used anywhere: the Poincaré
hypothesis is carried explicitly, and the interior estimates do not see the boundary.
Main declarations #
TauCeti.PDE.jetField: the value-gradient jet field of a Sobolev function.TauCeti.PDE.energyFormH1: the divergence-form energy form onH¹(Ω) = W^{1,2}(Ω).TauCeti.PDE.energyFormH1_const_eq_setIntegral: the energy form of a constant principal coefficient with no lower-order terms is the integral of⟨A ∇u, ∇v⟩.TauCeti.PDE.energyFormH1_comm_of_isSymm_ae: symmetry of the drift-free energy form under an almost everywhere symmetric principal coefficient.TauCeti.PDE.energyFormH1LandTauCeti.PDE.energyFormH1L0: the energy form bundled as a continuous bilinear map onH¹(Ω)and onH¹₀(Ω), built fromTauCeti.PDE.energyFormLpVariable.TauCeti.PDE.energyFormH1L0_comm: symmetry of the bundledH¹₀energy form, from symmetry of the energy form at the functions ofH¹₀(Ω).TauCeti.PDE.exists_forcing_energyFormH1_principal_eq: a weak equation with bounded lower-order coefficients gives a weak equation for its principal part with anL²forcing.TauCeti.PDE.UniformlyEllipticOn.integrable_energyIntegrand_jetField: the energy density of two Sobolev functions is integrable.TauCeti.PDE.UniformlyEllipticOn.norm_energyFormH1_le: boundedness of the energy form, with explicit constantΛ + β + γ.TauCeti.PDE.UniformlyEllipticOn.garding_energyFormH1_self: Gårding's inequality onH¹(Ω).TauCeti.PDE.UniformlyEllipticOn.garding_energyFormH1_self_norm: the equivalent roadmap form with anH¹norm and a negativeL²term.TauCeti.PDE.UniformlyEllipticOn.garding_energyFormH1_self_of_mass_lower_bound: the bound retaining an arbitrary mass floorδwith the half split.TauCeti.PDE.UniformlyEllipticOn.garding_energyFormH1_self_of_mass_lower_bound_with_parameter: the mass-floor bound with any positive Young parameter.TauCeti.PDE.UniformlyEllipticOn.min_mul_norm_sq_le_energyFormH1_self_of_mass_lower_bound: theH¹-norm lower bound with constantmin (λ/2) (δ - β²/(2λ)).TauCeti.PDE.UniformlyEllipticOn.mul_norm_sq_le_energyFormH1_self_of_poincare: the lower bound by‖u‖²_{H¹}obtained from a Poincaré inequality, andTauCeti.PDE.energyFormH1_poincare_constant_pos, the smallness conditionβP < λunder which it is coercivity.TauCeti.PDE.UniformlyEllipticOn.mul_norm_gradient_sq_le_energyFormH1_self_of_zero_drift: the lower boundλ‖∇u‖²_{L²} ≤ a(u, u)when the drift vanishes, andTauCeti.PDE.UniformlyEllipticOn.div_mul_norm_sq_le_energyFormH1_self_of_zero_drift: the correspondingH¹-norm lower bound for any function satisfying a Poincaré inequality.TauCeti.PDE.norm_energyFormH1L_le_of_bounds: the bundled form's operator-norm bound, stated from upper coefficient bounds without requiring lower ellipticity.TauCeti.PDE.UniformlyEllipticOn.mul_norm_sq_le_energyFormH1_self_of_subset_slabandTauCeti.PDE.UniformlyEllipticOn.mul_norm_sq_le_energyFormH1_self_of_subset_ball: lower bounds onH¹₀(Ω)for a domain trapped in a slab, or in a ball.
References #
Lane D, item 16 of TauCetiRoadmap/PDE/README.md; L. C. Evans, Partial Differential
Equations, Section 6.2 (energy estimates and Gårding's inequality); D. Gilbarg and
N. Trudinger, Elliptic Partial Differential Equations of Second Order, Chapter 8.
The jet field of a Sobolev function #
The value-gradient jet field x ↦ (u x, ∇u x) of a first-order Sobolev function.
This is the raw jet field that TauCeti.PDE.energyFormIntegral expects; the two components
are the Lᵖ classes TauCeti.W1p.value and TauCeti.W1p.gradient, so the jet field is only
determined almost everywhere on Ω, which is all an integrated energy form sees.
Its application theorem exposes the componentwise fact needed downstream.
Equations
- TauCeti.PDE.jetField u x = (↑↑(TauCeti.W1p.value u) x, ↑↑(TauCeti.W1p.gradient u) x)
Instances For
The value-gradient jet field evaluated at a point.
The jet field of a Sobolev function belongs to Lᵖ(Ω): both of its components do, by the
construction of W^{1,p}(Ω).
Bounded measurable coefficients define an essentially bounded field of pointwise energy forms. Only the displayed upper bound on the principal part is needed; ellipticity is not.
Subtracting a constant from the mass coefficient preserves essential boundedness of the pointwise energy forms.
The continuous linear inclusion that forgets the W^{1,2} weak-derivative constraint and
views a Sobolev function as its square-integrable value-gradient jet.
Equations
- TauCeti.PDE.jetLpL = ContinuousLinearMap.compLpL 2 (mu.restrict ↑Omega) ↑(WithLp.prodContinuousLinearEquiv 2 ℝ ℝ (EuclideanSpace ℝ ι)) ∘SL (↑(TauCeti.w1pSubmodule mu Omega 2)).subtypeL
Instances For
The L² jet inclusion agrees almost everywhere with jetField.
The squared gradient component of the Sobolev jet field is integrable.
The squared value component of the Sobolev jet field is integrable.
The integral of the squared gradient component of a Sobolev jet is the squared L²
gradient norm.
The integral of the squared value component of a Sobolev jet is the squared L² value
norm.
The L² norm of the jet field of a Sobolev function is at most its W^{1,2} norm: the jet
fibre ℝ × EuclideanSpace ℝ ι of the energy integrand carries the product sup norm, which is
dominated by the Hilbert graph norm of W^{1,2}(Ω).
Cauchy--Schwarz for jet fields. The integral of the product of the jet norms of two
Sobolev functions is at most the product of their W^{1,2} norms. This is the estimate that
turns the pointwise operator-norm bound on the energy integrand into boundedness of the energy
form.
The energy form on H¹(Ω) #
The divergence-form energy form on H¹(Ω) = W^{1,2}(Ω),
a(u, v) = ∫_Ω aⁱʲ ∂ᵢu ∂ⱼv + bⁱ ∂ᵢu v + c u v,
obtained by integrating the pointwise jet form TauCeti.PDE.energyIntegrand against the jet
fields of two Sobolev functions. The coefficients stay separate, explicit data: no
boundedness, ellipticity or measurability is assumed here, and each estimate below names the
hypotheses it needs.
Equations
- TauCeti.PDE.energyFormH1 a b c u v = TauCeti.PDE.energyFormIntegral (mu.restrict ↑Omega) a b c (TauCeti.PDE.jetField u) (TauCeti.PDE.jetField v)
Instances For
The energy form on H¹(Ω) is the integral of the pointwise energy density over Ω.
The constant-coefficient Dirichlet energy form. With a constant principal coefficient
matrix and no drift or mass term, the energy form on H¹(Ω) is the integral of ⟨A ∇u, ∇v⟩
over Ω. This is the shape the difference-quotient arguments of elliptic regularity work
with.
The Sobolev energy form vanishes at zero in its left argument.
The Sobolev energy form vanishes at zero in its right argument.
Homogeneity of the Sobolev energy form in its left argument.
Homogeneity of the Sobolev energy form in its right argument.
Symmetry of the energy form on H¹(Ω). With no drift and an almost everywhere symmetric
principal coefficient the divergence-form energy form is symmetric, which is what makes the
associated eigenvalue problem a self-adjoint one. The mass coefficient is unrestricted: it
enters the form through the symmetric term c u v.
The coefficient in
TauCeti.PDE.UniformlyEllipticOn.mul_norm_sq_le_energyFormH1_self_of_poincare is positive under the
smallness condition βP < λ relating the drift bound, the Poincaré constant and the ellipticity;
that is the sufficient condition under which the estimate is coercivity.
Shortcut seminormed group instance on W^{1,2}(Ω) to aid instance search for continuous
bilinear forms.
Instances For
Shortcut normed space instance on W^{1,2}(Ω) to aid instance search for continuous
bilinear forms.
Equations
Instances For
The energy density of two Sobolev functions is integrable whenever its pointwise bilinear coefficient field is essentially bounded.
Subtracting a constant from the mass coefficient subtracts the corresponding L² mass pairing
from the Sobolev energy form. No boundary or coercivity assumption is needed.
The energy form on H¹(Ω) as a continuous bilinear form, obtained by restricting the
existing variable-coefficient L² energy form along the continuous Sobolev jet inclusion.
Equations
- TauCeti.PDE.energyFormH1L hcoeff = (TauCeti.PDE.energyFormLpVariable (mu.restrict ↑Omega) a b c hcoeff).bilinearComp TauCeti.PDE.jetLpL TauCeti.PDE.jetLpL
Instances For
The bundled Sobolev energy form evaluates to energyFormH1.
Additivity of the Sobolev energy form in its left argument.
Additivity of the Sobolev energy form in its right argument.
Boundedness of the Sobolev energy form from upper bounds alone. No lower ellipticity hypothesis is needed.
The operator norm of the bundled Sobolev energy form is controlled by the coefficient upper bounds.
The energy form on H¹₀(Ω) as a continuous bilinear form, obtained by restricting
energyFormH1L along the closed-subspace inclusion.
Equations
- TauCeti.PDE.energyFormH1L0 hcoeff = (TauCeti.PDE.energyFormH1L hcoeff).bilinearComp (↑(TauCeti.w1p0Submodule mu Omega 2)).subtypeL (↑(TauCeti.w1p0Submodule mu Omega 2)).subtypeL
Instances For
The bundled H¹₀ energy form evaluates to energyFormH1 on the underlying Sobolev
functions.
Symmetry of the bundled H¹₀ energy form. Only symmetry of energyFormH1 at the
Sobolev functions underlying H¹₀(Ω) is needed; with no drift and an almost everywhere symmetric
principal coefficient TauCeti.PDE.energyFormH1_comm_of_isSymm_ae supplies it.
A weak equation with an essentially bounded principal energy density and bounded
lower-order coefficients admits an L² forcing for its principal part alone. Neither
ellipticity nor a boundary condition on the solution is required.
The energy density of two Sobolev functions is integrable on Ω, for uniformly elliptic
principal coefficients with bounded measurable lower-order terms. Both jets are L², so the
product of their norms, which dominates the density, is integrable by Cauchy--Schwarz.
Boundedness of the energy form on H¹(Ω). For a uniformly elliptic principal
coefficient with upper constant Λ, a drift bounded by β and a mass coefficient bounded by
γ,
|a(u, v)| ≤ (Λ + β + γ) ‖u‖_{H¹} ‖v‖_{H¹}.
The constant is the sum of the three coefficient bounds, an explicit pointwise operator-norm
bound for the energy integrand; the passage from the pointwise bound to the integrated one is
Cauchy--Schwarz. Together with garding_energyFormH1_self this is the pair of estimates the
energy method needs.
Gårding's inequality with a mass floor and any positive Young parameter ε. The
coefficients λ - ε and δ - β²/(4ε) can both be positive exactly when β² < 4λδ.
The estimate itself also holds when either coefficient is nonpositive.
Gårding's inequality with a lower bound δ for the mass coefficient. The gradient
coefficient is λ/2 and the value coefficient is δ - β²/(2λ). The estimate holds for
arbitrary δ, including negative lower bounds.
Gårding's inequality on H¹(Ω). For a uniformly elliptic principal coefficient with
lower constant λ, a drift bounded by β and a nonnegative mass coefficient,
(λ/2)‖∇u‖²_{L²} - (β²/2λ)‖u‖²_{L²} ≤ a(u, u)
for every u ∈ H¹(Ω). The drift is absorbed by Young's inequality at the cost of half of the
ellipticity floor, which is where the negative L² term comes from. Under the stated general
assumption c ≥ 0, either a Poincaré inequality or a sufficiently positive mass lower bound is
needed to eliminate that term.
Gårding's inequality in the roadmap's H¹-norm form. This is the equivalent
restatement
(λ/2)‖u‖²_{H¹} - (λ/2 + β²/2λ)‖u‖²_{L²} ≤ a(u,u).
A lower bound in the full Sobolev norm with constant min (λ - ε) (δ - β²/(4ε)).
Positive coefficients give coercivity on all of H¹(Ω), independently of the domain.
A lower bound for the energy form in the full H¹ norm, with constant
min (λ/2) (δ - β²/(2λ)). This gives coercivity on all of H¹(Ω) when δ > β²/(2λ),
without a Poincaré inequality or a boundary condition.
An energy-form lower bound from a Poincaré inequality. If u ∈ H¹(Ω) satisfies
‖u‖_{L²} ≤ P‖∇u‖_{L²} then
(λ² - β²P²)/(2λ(P² + 1)) · ‖u‖²_{H¹} ≤ a(u, u).
The estimate holds for every P for which the Poincaré bound is available; it is coercivity
once its constant is positive, for which TauCeti.PDE.energyFormH1_poincare_constant_pos supplies
the
sufficient smallness condition βP < λ relating the drift to the ellipticity and the domain.
The Poincaré hypothesis is carried on the single vector u, so a caller may supply it from
membership in W^{1,2}_0(Ω), as the slab and ball corollaries below do, or from any other
source.
The drift-free energy dominates the Dirichlet energy. When the drift vanishes on Ω
and the mass coefficient is nonnegative, uniform ellipticity integrates to
λ‖∇u‖²_{L²} ≤ a(u, u)
for every u ∈ H¹(Ω). With no drift there is nothing for Young's inequality to absorb, so this
keeps the full ellipticity constant where garding_energyFormH1_self is left with λ/2.
An H¹-norm lower bound with no drift. When the drift vanishes on Ω there is no
condition: a Poincaré inequality alone gives
λ/(P² + 1) · ‖u‖²_{H¹} ≤ a(u, u).
This is the case of a divergence-form operator -∂ⱼ(aⁱʲ ∂ᵢu) + c u. The constant is the one
the ellipticity floor gives directly, without the factor 2 that Young's inequality costs when
a drift has to be absorbed.
Energy-form lower bounds on slab- or ball-contained domains #
An energy-form lower bound on H¹₀(Ω) for a domain trapped in a slab. If
Ω ⊆ ℝ^{n+1} lies between the hyperplanes xᵢ = s and xᵢ = t, then every
u ∈ W^{1,2}_0(Ω) satisfies
(λ² - β²(t - s)²)/(2λ((t - s)² + 1)) · ‖u‖²_{H¹} ≤ a(u, u),
the Poincaré constant of the slab being its width t - s. The domain need not be bounded:
boundedness in one direction is enough, and no regularity of ∂Ω is used, the homogeneous
boundary condition being carried by membership in W^{1,2}_0(Ω).
An energy-form lower bound on H¹₀(Ω) for a domain inside a ball. For
Ω ⊆ B(z, R) ⊆ ℝ^{n+1} every u ∈ W^{1,2}_0(Ω) satisfies
(λ² - 4β²R²)/(2λ(4R² + 1)) · ‖u‖²_{H¹} ≤ a(u, u).
The Poincaré constant 2R is the diameter bound, not the sharp one, but it is explicit and
independent of the centre. Together with positivity of the displayed constant, this is the
diagonal estimate used to prove coercivity for a Lax--Milgram application.