Integrated divergence-form energy forms

The weak energy form of a divergence-form operator is

a(u, v) = ∫ aⁱʲ ∂ᵢu ∂ⱼv + bⁱ ∂ᵢu v + c u v.

The preceding PDE files build the pointwise jet integrand energyIntegrand (a x) (b x) (c x) and prove the measurability and integrability estimates needed to integrate it. This file performs that integration for raw jet fields U V : X → ℝ × EuclideanSpace ℝ n. It deliberately does not define a Sobolev space or weak derivative: the value-gradient jets of Sobolev functions can feed this definition.

Main declarations

• TauCeti.PDE.energyFormIntegral: the integrated scalar energy form on two jet fields.
• TauCeti.PDE.energyFormIntegral_one_zero_zero and TauCeti.PDE.energyFormIntegral_one_zero_mass: the −Δ and shifted-−Δ + c model forms.
• TauCeti.PDE.energyFormIntegral_add_left, TauCeti.PDE.energyFormIntegral_add_right, TauCeti.PDE.energyFormIntegral_smul_left, and TauCeti.PDE.energyFormIntegral_smul_right: bilinearity identities under the usual Bochner-integrability hypotheses.
• TauCeti.PDE.norm_energyFormIntegral_le_of_bounds: the integrated boundedness estimate obtained from the pointwise coefficient bounds.
• TauCeti.PDE.integral_min_lam_mass_mul_norm_sq_le_energyFormIntegral_zero_drift_self: the zero-drift integrated diagonal lower bound from a nonnegative principal quadratic lower bound and arbitrary mass.
• TauCeti.PDE.integral_mul_norm_snd_sq_le_energyFormIntegral_zero_drift_self: the integrated zero-drift lower bound for the squared gradient component.
• TauCeti.PDE.UniformlyEllipticOn.norm_energyFormIntegral_le_on: the corresponding boundedness estimate from uniform ellipticity on an a.e. domain.

@[instance_reducible]

noncomputable def TauCeti.PDE.integratedEnergyFormDecidableEq {n : Type u_2} : DecidableEq n

Local classical decidable equality for finite coordinate indices in integrated energy proofs.

Equations

• TauCeti.PDE.integratedEnergyFormDecidableEq = Classical.decEq n

noncomputable def TauCeti.PDE.energyFormIntegral {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U V : X → ℝ × EuclideanSpace ℝ n) : ℝ

The scalar energy form obtained by integrating the divergence-form pointwise jet integrand against a measure.

For a Sobolev function u, the intended jet field is x ↦ (u x, ∇u x). This definition stays at the raw-jet level because weak-derivative Sobolev spaces are a separate prerequisite.

Equations

• TauCeti.PDE.energyFormIntegral μ a b c U V = ∫ (x : X), ((TauCeti.PDE.energyIntegrand (a x) (b x) (c x)) (U x)) (V x) ∂μ

theorem TauCeti.PDE.energyFormIntegral_def {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U V : X → ℝ × EuclideanSpace ℝ n) : energyFormIntegral μ a b c U V = ∫ (x : X), ((energyIntegrand (a x) (b x) (c x)) (U x)) (V x) ∂μ

Unfolding rule for the integrated energy form.

theorem TauCeti.PDE.energyFormIntegral_congr_ae {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U V : X → ℝ × EuclideanSpace ℝ n) {a' : X → Matrix n n ℝ} {b' : X → EuclideanSpace ℝ n} {c' : X → ℝ} {U' V' : X → ℝ × EuclideanSpace ℝ n} (ha : a =ᵐ[μ] a') (hb : b =ᵐ[μ] b') (hc : c =ᵐ[μ] c') (hU : U =ᵐ[μ] U') (hV : V =ᵐ[μ] V') : energyFormIntegral μ a b c U V = energyFormIntegral μ a' b' c' U' V'

The integrated energy form respects almost-everywhere equality of all coefficient and jet fields.

@[simp]

theorem TauCeti.PDE.energyFormIntegral_zero_left {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (V : X → ℝ × EuclideanSpace ℝ n) : energyFormIntegral μ a b c (fun (x : X) => 0) V = 0

The integrated energy form vanishes when the left jet field is zero.

@[simp]

theorem TauCeti.PDE.energyFormIntegral_zero_right {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U : X → ℝ × EuclideanSpace ℝ n) : (energyFormIntegral μ a b c U fun (x : X) => 0) = 0

The integrated energy form vanishes when the right jet field is zero.

@[simp]

theorem TauCeti.PDE.energyFormIntegral_zero_coefficients {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (U V : X → ℝ × EuclideanSpace ℝ n) : energyFormIntegral μ (fun (x : X) => 0) (fun (x : X) => 0) (fun (x : X) => 0) U V = 0

The zero coefficient triple gives the zero integrated energy form.

@[simp]

theorem TauCeti.PDE.energyFormIntegral_neg_left {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U V : X → ℝ × EuclideanSpace ℝ n) : energyFormIntegral μ a b c (fun (x : X) => -U x) V = -energyFormIntegral μ a b c U V

Negating the left jet field negates the integrated energy form.

@[simp]

theorem TauCeti.PDE.energyFormIntegral_neg_right {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U V : X → ℝ × EuclideanSpace ℝ n) : (energyFormIntegral μ a b c U fun (x : X) => -V x) = -energyFormIntegral μ a b c U V

Negating the right jet field negates the integrated energy form.

@[simp]

theorem TauCeti.PDE.energyFormIntegral_neg_coefficients {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U V : X → ℝ × EuclideanSpace ℝ n) : energyFormIntegral μ (fun (x : X) => -a x) (fun (x : X) => -b x) (fun (x : X) => -c x) U V = -energyFormIntegral μ a b c U V

Negating the coefficient triple negates the integrated energy form.

theorem TauCeti.PDE.energyFormIntegral_add_left {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U V W : X → ℝ × EuclideanSpace ℝ n) (hU : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (V x)) μ) (hW : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) (b x) (c x)) (W x)) (V x)) μ) : energyFormIntegral μ a b c (fun (x : X) => U x + W x) V = energyFormIntegral μ a b c U V + energyFormIntegral μ a b c W V

Additivity in the left jet field, assuming the two summand energy densities are integrable.

theorem TauCeti.PDE.energyFormIntegral_add_right {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U V W : X → ℝ × EuclideanSpace ℝ n) (hV : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (V x)) μ) (hW : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (W x)) μ) : (energyFormIntegral μ a b c U fun (x : X) => V x + W x) = energyFormIntegral μ a b c U V + energyFormIntegral μ a b c U W

Additivity in the right jet field, assuming the two summand energy densities are integrable.

theorem TauCeti.PDE.energyFormIntegral_smul_left {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U V : X → ℝ × EuclideanSpace ℝ n) (r : ℝ) : energyFormIntegral μ a b c (fun (x : X) => r • U x) V = r * energyFormIntegral μ a b c U V

Homogeneity in the left jet field.

theorem TauCeti.PDE.energyFormIntegral_smul_right {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U V : X → ℝ × EuclideanSpace ℝ n) (r : ℝ) : (energyFormIntegral μ a b c U fun (x : X) => r • V x) = r * energyFormIntegral μ a b c U V

Homogeneity in the right jet field.

theorem TauCeti.PDE.energyFormIntegral_add {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U V : X → ℝ × EuclideanSpace ℝ n) (a' : X → Matrix n n ℝ) (b' : X → EuclideanSpace ℝ n) (c' : X → ℝ) (h : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (V x)) μ) (h' : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a' x) (b' x) (c' x)) (U x)) (V x)) μ) : energyFormIntegral μ (fun (x : X) => a x + a' x) (fun (x : X) => b x + b' x) (fun (x : X) => c x + c' x) U V = energyFormIntegral μ a b c U V + energyFormIntegral μ a' b' c' U V

The integrated energy form is additive in the coefficient triple, under the corresponding integrability assumptions for the two summand densities.

theorem TauCeti.PDE.energyFormIntegral_sub {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U V : X → ℝ × EuclideanSpace ℝ n) (a' : X → Matrix n n ℝ) (b' : X → EuclideanSpace ℝ n) (c' : X → ℝ) (h : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (V x)) μ) (h' : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a' x) (b' x) (c' x)) (U x)) (V x)) μ) : energyFormIntegral μ (fun (x : X) => a x - a' x) (fun (x : X) => b x - b' x) (fun (x : X) => c x - c' x) U V = energyFormIntegral μ a b c U V - energyFormIntegral μ a' b' c' U V

The integrated energy form is subtractive in the coefficient triple, under the corresponding integrability assumptions for the two densities.

theorem TauCeti.PDE.energyFormIntegral_smul {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U V : X → ℝ × EuclideanSpace ℝ n) (r : ℝ) : energyFormIntegral μ (fun (x : X) => r • a x) (fun (x : X) => r • b x) (fun (x : X) => r * c x) U V = r * energyFormIntegral μ a b c U V

The integrated energy form is homogeneous in the coefficient triple.

theorem TauCeti.PDE.energyFormIntegral_principal_add_lowerOrder {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U V : X → ℝ × EuclideanSpace ℝ n) (hprincipal : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) 0 0) (U x)) (V x)) μ) (hlower : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand 0 (b x) (c x)) (U x)) (V x)) μ) : energyFormIntegral μ a b c U V = energyFormIntegral μ a (fun (x : X) => 0) (fun (x : X) => 0) U V + energyFormIntegral μ (fun (x : X) => 0) b c U V

The integrated full energy form splits into its principal and lower-order parts.

theorem TauCeti.PDE.energyFormIntegral_principal_drift_mass {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U V : X → ℝ × EuclideanSpace ℝ n) (hprincipal : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) 0 0) (U x)) (V x)) μ) (hdrift : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand 0 (b x) 0) (U x)) (V x)) μ) (hmass : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand 0 0 (c x)) (U x)) (V x)) μ) : energyFormIntegral μ a b c U V = energyFormIntegral μ a (fun (x : X) => 0) (fun (x : X) => 0) U V + energyFormIntegral μ (fun (x : X) => 0) b (fun (x : X) => 0) U V + energyFormIntegral μ (fun (x : X) => 0) (fun (x : X) => 0) c U V

The integrated full energy form splits into its principal, drift, and mass pieces.

theorem TauCeti.PDE.energyFormIntegral_eq_one_zero_baseMass_add_perturbation {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U V : X → ℝ × EuclideanSpace ℝ n) (m : X → ℝ) (hmodel : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand 1 0 (m x)) (U x)) (V x)) μ) (hpert : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x - 1) (b x) (c x - m x)) (U x)) (V x)) μ) : energyFormIntegral μ a b c U V = energyFormIntegral μ (fun (x : X) => 1) (fun (x : X) => 0) m U V + energyFormIntegral μ (fun (x : X) => a x - 1) b (fun (x : X) => c x - m x) U V

The integrated full energy form is a shifted-Laplacian model plus the residual coefficient perturbation.

theorem TauCeti.PDE.energyFormIntegral_eq_one_zero_mass_add_perturbation {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U V : X → ℝ × EuclideanSpace ℝ n) (hmodel : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand 1 0 (c x)) (U x)) (V x)) μ) (hpert : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x - 1) (b x) 0) (U x)) (V x)) μ) : energyFormIntegral μ a b c U V = energyFormIntegral μ (fun (x : X) => 1) (fun (x : X) => 0) c U V + energyFormIntegral μ (fun (x : X) => a x - 1) b (fun (x : X) => 0) U V

The integrated full energy form is the shifted-Laplacian form with the same mass plus the principal-and-drift perturbation.

theorem TauCeti.PDE.energyFormIntegral_one_zero_zero {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (U V : X → ℝ × EuclideanSpace ℝ n) : energyFormIntegral μ (fun (x : X) => 1) (fun (x : X) => 0) (fun (x : X) => 0) U V = ∫ (x : X), (V x).2.ofLp ⬝ᵥ (U x).2.ofLp ∂μ

The integrated −Δ model form is the integral of the dot product of the two gradient components of the jet fields.

theorem TauCeti.PDE.energyFormIntegral_one_zero_mass {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (U V : X → ℝ × EuclideanSpace ℝ n) (m : X → ℝ) : energyFormIntegral μ (fun (x : X) => 1) (fun (x : X) => 0) m U V = ∫ (x : X), (V x).2.ofLp ⬝ᵥ (U x).2.ofLp + m x * (U x).1 * (V x).1 ∂μ

The integrated shifted Laplacian model form −Δ + c is the sum of the Dirichlet density and the mass density.

theorem TauCeti.PDE.energyFormIntegral_one_zero_mass_self {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (U : X → ℝ × EuclideanSpace ℝ n) (m : X → ℝ) : energyFormIntegral μ (fun (x : X) => 1) (fun (x : X) => 0) m U U = ∫ (x : X), ‖(U x).2‖ ^ 2 + m x * (U x).1 ^ 2 ∂μ

The diagonal of the integrated shifted Laplacian model is the integral of ‖∇u‖² + c u² at the jet level.

theorem TauCeti.PDE.norm_energyFormIntegral_le_of_bounds {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U V : X → ℝ × EuclideanSpace ℝ n) {Lam beta gamma : ℝ} (hLam : 0 ≤ Lam) (ha : ∀ᵐ (x : X) ∂μ, ∀ (η ξ : EuclideanSpace ℝ n), |η.ofLp ⬝ᵥ (a x).mulVec ξ.ofLp| ≤ Lam * ‖η‖ * ‖ξ‖) (hb : ∀ᵐ (x : X) ∂μ, ‖b x‖ ≤ beta) (hc : ∀ᵐ (x : X) ∂μ, ‖c x‖ ≤ gamma) (hUV : MeasureTheory.Integrable (fun (x : X) => (Lam + beta + gamma) * (‖U x‖ * ‖V x‖)) μ) : ‖energyFormIntegral μ a b c U V‖ ≤ ∫ (x : X), (Lam + beta + gamma) * (‖U x‖ * ‖V x‖) ∂μ

Integrated boundedness of the raw-jet energy form from a.e. coefficient bounds.

This is the scalar integral version of norm_energyIntegrand_apply_le_of_bounds: if the pointwise jet product ‖U x‖ * ‖V x‖ is integrable, the absolute value of the integrated form is bounded by (Λ + β + γ) times its integral.

theorem TauCeti.PDE.garding_energyFormIntegral_self_of_bounds {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U : X → ℝ × EuclideanSpace ℝ n) {beta lam : ℝ} (hlam : 0 < lam) (ha : ∀ᵐ (x : X) ∂μ, ∀ (ξ : EuclideanSpace ℝ n), lam * ‖ξ‖ ^ 2 ≤ ξ.ofLp ⬝ᵥ (a x).mulVec ξ.ofLp) (hb : ∀ᵐ (x : X) ∂μ, ‖b x‖ ≤ beta) (hc : ∀ᵐ (x : X) ∂μ, 0 ≤ c x) (hlower : MeasureTheory.Integrable (fun (x : X) => lam / 2 * ‖(U x).2‖ ^ 2 - beta ^ 2 / (2 * lam) * (U x).1 ^ 2) μ) (henergy : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (U x)) μ) : ∫ (x : X), lam / 2 * ‖(U x).2‖ ^ 2 - beta ^ 2 / (2 * lam) * (U x).1 ^ 2 ∂μ ≤ energyFormIntegral μ a b c U U

Integrated Gårding lower bound from a.e. lower ellipticity and a.e. lower-order coefficient hypotheses.

theorem TauCeti.PDE.garding_energyFormIntegral_self_of_mass_lower_bound_of_bounds_with_parameter {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U : X → ℝ × EuclideanSpace ℝ n) {beta lam mu eps : ℝ} (heps : 0 < eps) (ha : ∀ᵐ (x : X) ∂μ, ∀ (ξ : EuclideanSpace ℝ n), lam * ‖ξ‖ ^ 2 ≤ ξ.ofLp ⬝ᵥ (a x).mulVec ξ.ofLp) (hb : ∀ᵐ (x : X) ∂μ, ‖b x‖ ≤ beta) (hc : ∀ᵐ (x : X) ∂μ, mu ≤ c x) (hlower : MeasureTheory.Integrable (fun (x : X) => (lam - eps) * ‖(U x).2‖ ^ 2 + (mu - beta ^ 2 / (4 * eps)) * (U x).1 ^ 2) μ) (henergy : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (U x)) μ) : ∫ (x : X), (lam - eps) * ‖(U x).2‖ ^ 2 + (mu - beta ^ 2 / (4 * eps)) * (U x).1 ^ 2 ∂μ ≤ energyFormIntegral μ a b c U U

The integrated mass-floor Gårding bound with a free positive Young parameter. The principal lower bound and both lower-order coefficient bounds need hold only almost everywhere.

theorem TauCeti.PDE.garding_energyFormIntegral_self_of_mass_lower_bound_of_bounds {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U : X → ℝ × EuclideanSpace ℝ n) {beta lam mu : ℝ} (hlam : 0 < lam) (ha : ∀ᵐ (x : X) ∂μ, ∀ (ξ : EuclideanSpace ℝ n), lam * ‖ξ‖ ^ 2 ≤ ξ.ofLp ⬝ᵥ (a x).mulVec ξ.ofLp) (hb : ∀ᵐ (x : X) ∂μ, ‖b x‖ ≤ beta) (hc : ∀ᵐ (x : X) ∂μ, mu ≤ c x) (hlower : MeasureTheory.Integrable (fun (x : X) => lam / 2 * ‖(U x).2‖ ^ 2 + (mu - beta ^ 2 / (2 * lam)) * (U x).1 ^ 2) μ) (henergy : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (U x)) μ) : ∫ (x : X), lam / 2 * ‖(U x).2‖ ^ 2 + (mu - beta ^ 2 / (2 * lam)) * (U x).1 ^ 2 ∂μ ≤ energyFormIntegral μ a b c U U

Integrated Gårding lower bound with a mass floor from a.e. lower ellipticity and a.e. lower-order coefficient hypotheses.

theorem TauCeti.PDE.integral_min_lam_mass_mul_norm_sq_le_energyFormIntegral_zero_drift_self {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (c : X → ℝ) (U : X → ℝ × EuclideanSpace ℝ n) {lam : ℝ} (hlam : 0 ≤ lam) (ha : ∀ᵐ (x : X) ∂μ, ∀ (ξ : EuclideanSpace ℝ n), lam * ‖ξ‖ ^ 2 ≤ ξ.ofLp ⬝ᵥ (a x).mulVec ξ.ofLp) (hlower : MeasureTheory.Integrable (fun (x : X) => min lam (c x) * ‖U x‖ ^ 2) μ) (henergy : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) 0 (c x)) (U x)) (U x)) μ) : ∫ (x : X), min lam (c x) * ‖U x‖ ^ 2 ∂μ ≤ energyFormIntegral μ a (fun (x : X) => 0) c U U

Integrated zero-drift diagonal lower bound from an a.e. nonnegative principal quadratic lower bound and an arbitrary mass coefficient.

theorem TauCeti.PDE.integral_mul_norm_snd_sq_le_energyFormIntegral_zero_drift_self {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (c : X → ℝ) (U : X → ℝ × EuclideanSpace ℝ n) {lam : ℝ} (ha : ∀ᵐ (x : X) ∂μ, ∀ (ξ : EuclideanSpace ℝ n), lam * ‖ξ‖ ^ 2 ≤ ξ.ofLp ⬝ᵥ (a x).mulVec ξ.ofLp) (hc : ∀ᵐ (x : X) ∂μ, 0 ≤ c x) (hlower : MeasureTheory.Integrable (fun (x : X) => lam * ‖(U x).2‖ ^ 2) μ) (henergy : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) 0 (c x)) (U x)) (U x)) μ) : ∫ (x : X), lam * ‖(U x).2‖ ^ 2 ∂μ ≤ energyFormIntegral μ a (fun (x : X) => 0) c U U

An integrated zero-drift energy form dominates the integral of the squared gradient component under an a.e. principal quadratic lower bound and nonnegative mass coefficient.

theorem TauCeti.PDE.energyFormIntegral_zero_drift_self_nonneg {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (c : X → ℝ) (U : X → ℝ × EuclideanSpace ℝ n) (ha : ∀ᵐ (x : X) ∂μ, ∀ (ξ : EuclideanSpace ℝ n), 0 ≤ ξ.ofLp ⬝ᵥ (a x).mulVec ξ.ofLp) (hc : ∀ᵐ (x : X) ∂μ, 0 ≤ c x) : 0 ≤ energyFormIntegral μ a (fun (x : X) => 0) c U U

A zero-drift diagonal integrated energy form is nonnegative when the principal quadratic form and mass coefficient are a.e. nonnegative.

theorem TauCeti.PDE.integral_min_diagonal_lower_bound_mul_norm_sq_le_energyFormIntegral_self_of_bounds {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (U : X → ℝ × EuclideanSpace ℝ n) {beta lam mu : ℝ} (hlam : 0 < lam) (ha : ∀ᵐ (x : X) ∂μ, ∀ (ξ : EuclideanSpace ℝ n), lam * ‖ξ‖ ^ 2 ≤ ξ.ofLp ⬝ᵥ (a x).mulVec ξ.ofLp) (hb : ∀ᵐ (x : X) ∂μ, ‖b x‖ ≤ beta) (hc : ∀ᵐ (x : X) ∂μ, mu ≤ c x) (hlower : MeasureTheory.Integrable (fun (x : X) => min (lam / 2) (mu - beta ^ 2 / (2 * lam)) * ‖U x‖ ^ 2) μ) (henergy : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (U x)) μ) : ∫ (x : X), min (lam / 2) (mu - beta ^ 2 / (2 * lam)) * ‖U x‖ ^ 2 ∂μ ≤ energyFormIntegral μ a b c U U

Integrated explicit diagonal lower bound from a.e. lower ellipticity, a.e. lower-order coefficient hypotheses, allowing a signed mass floor.

theorem TauCeti.PDE.UniformlyEllipticOn.norm_energyFormIntegral_le_on {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) {Ω : Set X} {lam Lam beta gamma : ℝ} {a : X → Matrix n n ℝ} {b : X → EuclideanSpace ℝ n} {c : X → ℝ} {U V : X → ℝ × EuclideanSpace ℝ n} (h : UniformlyEllipticOn Ω a lam Lam) (hΩ : ∀ᵐ (x : X) ∂μ, x ∈ Ω) (hb : ∀ᵐ (x : X) ∂μ, ‖b x‖ ≤ beta) (hc : ∀ᵐ (x : X) ∂μ, ‖c x‖ ≤ gamma) (hUV : MeasureTheory.Integrable (fun (x : X) => (Lam + beta + gamma) * (‖U x‖ * ‖V x‖)) μ) : ‖energyFormIntegral μ a b c U V‖ ≤ ∫ (x : X), (Lam + beta + gamma) * (‖U x‖ * ‖V x‖) ∂μ

Integrated boundedness of the energy form from uniform ellipticity and a.e. lower-order coefficient bounds.

theorem TauCeti.PDE.UniformlyEllipticOn.garding_energyFormIntegral_self_on {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) {Ω : Set X} {lam Lam beta : ℝ} {a : X → Matrix n n ℝ} {b : X → EuclideanSpace ℝ n} {c : X → ℝ} {U : X → ℝ × EuclideanSpace ℝ n} (h : UniformlyEllipticOn Ω a lam Lam) (hΩ : ∀ᵐ (x : X) ∂μ, x ∈ Ω) (hb : ∀ᵐ (x : X) ∂μ, ‖b x‖ ≤ beta) (hc : ∀ᵐ (x : X) ∂μ, 0 ≤ c x) (hlower : MeasureTheory.Integrable (fun (x : X) => lam / 2 * ‖(U x).2‖ ^ 2 - beta ^ 2 / (2 * lam) * (U x).1 ^ 2) μ) (henergy : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (U x)) μ) : ∫ (x : X), lam / 2 * ‖(U x).2‖ ^ 2 - beta ^ 2 / (2 * lam) * (U x).1 ^ 2 ∂μ ≤ energyFormIntegral μ a b c U U

Integrated Gårding lower bound from uniform ellipticity and a.e. lower-order coefficient hypotheses.

theorem TauCeti.PDE.UniformlyEllipticOn.garding_energyFormIntegral_self_of_mass_lower_bound_with_parameter_on {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) {Ω : Set X} {lam Lam beta mu : ℝ} {a : X → Matrix n n ℝ} {b : X → EuclideanSpace ℝ n} {c : X → ℝ} {U : X → ℝ × EuclideanSpace ℝ n} (h : UniformlyEllipticOn Ω a lam Lam) (hΩ : ∀ᵐ (x : X) ∂μ, x ∈ Ω) (hb : ∀ᵐ (x : X) ∂μ, ‖b x‖ ≤ beta) (hc : ∀ᵐ (x : X) ∂μ, mu ≤ c x) {eps : ℝ} (heps : 0 < eps) (hlower : MeasureTheory.Integrable (fun (x : X) => (lam - eps) * ‖(U x).2‖ ^ 2 + (mu - beta ^ 2 / (4 * eps)) * (U x).1 ^ 2) μ) (henergy : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (U x)) μ) : ∫ (x : X), (lam - eps) * ‖(U x).2‖ ^ 2 + (mu - beta ^ 2 / (4 * eps)) * (U x).1 ^ 2 ∂μ ≤ energyFormIntegral μ a b c U U

The integrated mass-floor Gårding bound with uniform ellipticity and any positive Young parameter. The drift bound and mass floor are required only almost everywhere.

theorem TauCeti.PDE.UniformlyEllipticOn.garding_energyFormIntegral_self_of_mass_lower_bound_on {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) {Ω : Set X} {lam Lam beta mu : ℝ} {a : X → Matrix n n ℝ} {b : X → EuclideanSpace ℝ n} {c : X → ℝ} {U : X → ℝ × EuclideanSpace ℝ n} (h : UniformlyEllipticOn Ω a lam Lam) (hΩ : ∀ᵐ (x : X) ∂μ, x ∈ Ω) (hb : ∀ᵐ (x : X) ∂μ, ‖b x‖ ≤ beta) (hc : ∀ᵐ (x : X) ∂μ, mu ≤ c x) (hlower : MeasureTheory.Integrable (fun (x : X) => lam / 2 * ‖(U x).2‖ ^ 2 + (mu - beta ^ 2 / (2 * lam)) * (U x).1 ^ 2) μ) (henergy : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (U x)) μ) : ∫ (x : X), lam / 2 * ‖(U x).2‖ ^ 2 + (mu - beta ^ 2 / (2 * lam)) * (U x).1 ^ 2 ∂μ ≤ energyFormIntegral μ a b c U U

Integrated Gårding lower bound with a mass floor from uniform ellipticity and a.e. coefficient hypotheses.

theorem TauCeti.PDE.UniformlyEllipticOn.integral_min_diagonal_lower_bound_mul_norm_sq_le_energyFormIntegral_self_on {X : Type u_1} {n : Type u_2} [MeasurableSpace X] [Fintype n] (μ : MeasureTheory.Measure X) {Ω : Set X} {lam Lam beta mu : ℝ} {a : X → Matrix n n ℝ} {b : X → EuclideanSpace ℝ n} {c : X → ℝ} {U : X → ℝ × EuclideanSpace ℝ n} (h : UniformlyEllipticOn Ω a lam Lam) (hΩ : ∀ᵐ (x : X) ∂μ, x ∈ Ω) (hb : ∀ᵐ (x : X) ∂μ, ‖b x‖ ≤ beta) (hc : ∀ᵐ (x : X) ∂μ, mu ≤ c x) (hlower : MeasureTheory.Integrable (fun (x : X) => min (lam / 2) (mu - beta ^ 2 / (2 * lam)) * ‖U x‖ ^ 2) μ) (henergy : MeasureTheory.Integrable (fun (x : X) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (U x)) μ) : ∫ (x : X), min (lam / 2) (mu - beta ^ 2 / (2 * lam)) * ‖U x‖ ^ 2 ∂μ ≤ energyFormIntegral μ a b c U U

Integrated explicit diagonal lower bound from uniform ellipticity, a.e. coefficient hypotheses, allowing a signed mass floor.