Energy-integrand estimates from uniform ellipticity

TauCeti.Analysis.PDE.EnergyForm.Basic and TauCeti.Analysis.PDE.EnergyLowerBounds prove the pointwise estimates for divergence-form energy integrands from raw coefficient bounds. This file packages the same estimates for callers that hold the principal coefficient hypothesis UniformlyEllipticOn Ω a λ Λ.

The statements are still pointwise finite-dimensional estimates on jets ℝ × EuclideanSpace ℝ n, not integrated Sobolev-space theorems, and they are not the hypothesis of Lax--Milgram: that needs coercivity of the integrated form on a complete inner-product (H¹-type) space. They are the pointwise boundedness and diagonal lower bounds that the integrated inequality of TauCeti.Analysis.PDE.EnergyForm.Integrated.Basic consumes after integrating over the domain.

This file deliberately leaves symmetry to TauCeti.Analysis.PDE.SymmetricEnergy. For a zero-drift uniformly elliptic operator with symmetric principal coefficient, use UniformlyEllipticOn.min_diagonal_lower_bound_mul_norm_sq_le_energyIntegrand_self for the diagonal lower bound and the energyIntegrand_zero_drift_flip_eq_* lemmas for symmetry; for nonsymmetric coefficients, the symmetric-part API in TauCeti.Analysis.PDE.Ellipticity.Basic preserves the ellipticity constants before applying the same symmetry lemmas.

Main declarations

• TauCeti.PDE.UniformlyEllipticOn.norm_energyIntegrand_apply_le: pointwise boundedness of the full energy integrand from a uniform ellipticity hypothesis and bounds on the lower-order coefficients at that point.
• TauCeti.PDE.UniformlyEllipticOn.opNorm_energyIntegrand_le: operator-norm boundedness of the full energy integrand, with explicit constant Λ + β + γ.
• TauCeti.PDE.UniformlyEllipticOn.garding_energyIntegrand_self: the pointwise Gårding lower bound obtained from the lower ellipticity projection of UniformlyEllipticOn.
• TauCeti.PDE.UniformlyEllipticOn.garding_energyIntegrand_self_of_mass_lower_bound: the pointwise Gårding lower bound with a mass floor.
• TauCeti.PDE.UniformlyEllipticOn.min_diagonal_lower_bound_mul_norm_sq_le_energyIntegrand_self: the explicit diagonal estimate for a signed mass floor.
• TauCeti.PDE.UniformlyEllipticOn.min_lam_mass_mul_norm_sq_le_energyIntegrand_zero_drift_self: the zero-drift diagonal estimate from uniform ellipticity and arbitrary mass.
• TauCeti.PDE.UniformlyEllipticOn.mul_norm_snd_sq_le_energyIntegrand_zero_drift_self: the zero-drift lower bound for the squared gradient component.

theorem TauCeti.PDE.UniformlyEllipticOn.norm_energyIntegrand_apply_le {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam beta gamma : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {x : X} (hx : x ∈ Ω) {b₀ : EuclideanSpace ℝ n} {c₀ : ℝ} (hb : ‖b₀‖ ≤ beta) (hc : ‖c₀‖ ≤ gamma) (U V : ℝ × EuclideanSpace ℝ n) : ‖((energyIntegrand (a x) b₀ c₀) U) V‖ ≤ (Lam + beta + gamma) * ‖U‖ * ‖V‖

Pointwise boundedness of the energy integrand from uniform ellipticity of the principal coefficient and pointwise bounds on the drift and mass coefficients.

theorem TauCeti.PDE.UniformlyEllipticOn.opNorm_energyIntegrand_le {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam beta gamma : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {x : X} (hx : x ∈ Ω) {b₀ : EuclideanSpace ℝ n} {c₀ : ℝ} (hb : ‖b₀‖ ≤ beta) (hc : ‖c₀‖ ≤ gamma) : ‖energyIntegrand (a x) b₀ c₀‖ ≤ Lam + beta + gamma

Operator-norm boundedness of the energy integrand from uniform ellipticity of the principal coefficient and pointwise bounds on the drift and mass coefficients.

theorem TauCeti.PDE.UniformlyEllipticOn.garding_energyIntegrand_self {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam beta : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {x : X} (hx : x ∈ Ω) {b₀ : EuclideanSpace ℝ n} {c₀ : ℝ} (hb : ‖b₀‖ ≤ beta) (hc : 0 ≤ c₀) (U : ℝ × EuclideanSpace ℝ n) : lam / 2 * ‖U.2‖ ^ 2 - beta ^ 2 / (2 * lam) * U.1 ^ 2 ≤ ((energyIntegrand (a x) b₀ c₀) U) U

Pointwise Gårding inequality for a uniformly elliptic principal coefficient.

With nonnegative mass coefficient and drift bound β, the diagonal energy density is bounded below by (λ/2)‖∇u‖² - (β²/2λ)|u|².

theorem TauCeti.PDE.UniformlyEllipticOn.garding_energyIntegrand_self_of_mass_lower_bound_with_parameter {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam beta mu : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {x : X} (hx : x ∈ Ω) {b₀ : EuclideanSpace ℝ n} {c₀ eps : ℝ} (hb : ‖b₀‖ ≤ beta) (hc : mu ≤ c₀) (heps : 0 < eps) (U : ℝ × EuclideanSpace ℝ n) : (lam - eps) * ‖U.2‖ ^ 2 + (mu - beta ^ 2 / (4 * eps)) * U.1 ^ 2 ≤ ((energyIntegrand (a x) b₀ c₀) U) U

Pointwise Gårding lower bound with a mass floor for a uniformly elliptic principal coefficient.

For any ε > 0, the gradient coefficient is λ - ε and the value coefficient is μ - β²/(4ε). The estimate also holds when either coefficient is nonpositive.

theorem TauCeti.PDE.UniformlyEllipticOn.garding_energyIntegrand_self_of_mass_lower_bound {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam beta mu : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {x : X} (hx : x ∈ Ω) {b₀ : EuclideanSpace ℝ n} {c₀ : ℝ} (hb : ‖b₀‖ ≤ beta) (hc : mu ≤ c₀) (U : ℝ × EuclideanSpace ℝ n) : lam / 2 * ‖U.2‖ ^ 2 + (mu - beta ^ 2 / (2 * lam)) * U.1 ^ 2 ≤ ((energyIntegrand (a x) b₀ c₀) U) U

Pointwise Gårding lower bound with a mass floor for a uniformly elliptic principal coefficient.

With drift bound β and mass lower bound μ, the diagonal energy density is bounded below by (λ / 2)‖∇u‖² + (μ - β² / (2λ))u².

theorem TauCeti.PDE.UniformlyEllipticOn.min_diagonal_lower_bound_mul_norm_sq_le_energyIntegrand_self {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam beta mu : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {x : X} (hx : x ∈ Ω) {b₀ : EuclideanSpace ℝ n} {c₀ : ℝ} (hb : ‖b₀‖ ≤ beta) (hc : mu ≤ c₀) (U : ℝ × EuclideanSpace ℝ n) : min (lam / 2) (mu - beta ^ 2 / (2 * lam)) * ‖U‖ ^ 2 ≤ ((energyIntegrand (a x) b₀ c₀) U) U

The lower-bound estimate implies the explicit diagonal estimate with constant min (λ / 2) (μ - β² / (2λ)), allowing the second coefficient to have either sign.

theorem TauCeti.PDE.UniformlyEllipticOn.min_lam_mass_mul_norm_sq_le_energyIntegrand_zero_drift_self {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {x : X} (hx : x ∈ Ω) {c₀ : ℝ} (U : ℝ × EuclideanSpace ℝ n) : min lam c₀ * ‖U‖ ^ 2 ≤ ((energyIntegrand (a x) 0 c₀) U) U

Zero-drift diagonal lower bound for a uniformly elliptic principal coefficient and an arbitrary mass coefficient.

theorem TauCeti.PDE.UniformlyEllipticOn.mul_norm_snd_sq_le_energyIntegrand_zero_drift_self {X : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] {Ω : Set X} {a : X → Matrix n n ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) {x : X} (hx : x ∈ Ω) {c₀ : ℝ} (hc : 0 ≤ c₀) (U : ℝ × EuclideanSpace ℝ n) : lam * ‖U.2‖ ^ 2 ≤ ((energyIntegrand (a x) 0 c₀) U) U

A zero-drift energy density for a uniformly elliptic principal coefficient dominates the squared gradient component when the mass coefficient is nonnegative.