Integrability of pointwise PDE energy densities

The weak-form lane of the PDE roadmap will define the energy bilinear form by integrating the pointwise scalar density x ↦ energyIntegrand (a x) (b x) (c x) (U x) (V x). The preceding finite-dimensional files give the measurability of this density and the pointwise bound with explicit coefficient constants. This file packages the next handoff: bounded measurable coefficient fields and measurable jet fields whose norm product is integrable produce integrable scalar energy densities. In particular, this applies to square-integrable jet fields, and specializes on finite-measure domains to bounded jet fields.

This remains below the Sobolev-space construction. The coefficient bounds are stated inline, matching the roadmap's bounded-measurable-coefficient hypotheses.

Main declarations

• TauCeti.PDE.integrable_energyIntegrand_apply₂_of_integrable_norm_mul: coefficient bounds and an integrable product of jet norms give scalar-density integrability.
• TauCeti.PDE.integrable_energyIntegrand_apply₂_of_memLp_two: coefficient bounds and square-integrable jet fields give scalar-density integrability.
• TauCeti.PDE.integrable_energyIntegrand_apply₂_of_bounds: the bounded finite-measure specialization.
• TauCeti.PDE.integrable_energyIntegrand_apply_of_bounds: the fixed-jet specialization.
• The corresponding UniformlyEllipticOn.*_on lemmas replace the raw principal coefficient bound by the roadmap's named uniform-ellipticity hypothesis on an a.e.-supported domain.

@[instance_reducible]

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

Local classical decidable equality for finite coordinate indices in uniform-ellipticity wrappers.

Equations

• TauCeti.PDE.energyFormIntegrabilityDecidableEq = Classical.decEq n

theorem TauCeti.PDE.integrable_energyIntegrand_apply₂_of_integrable_norm_mul {α : Type u_1} {n : Type u_2} [MeasurableSpace α] [Fintype n] {μ : MeasureTheory.Measure α} {a : α → Matrix n n ℝ} {b : α → EuclideanSpace ℝ n} {c : α → ℝ} {U V : α → ℝ × EuclideanSpace ℝ n} {Lam beta gamma : ℝ} (hLam : 0 ≤ Lam) (ha : MeasureTheory.AEStronglyMeasurable a μ) (hb : MeasureTheory.AEStronglyMeasurable b μ) (hc : MeasureTheory.AEStronglyMeasurable c μ) (hU : MeasureTheory.AEStronglyMeasurable U μ) (hV : MeasureTheory.AEStronglyMeasurable V μ) (ha_bound : ∀ᵐ (x : α) ∂μ, ∀ (η ξ : EuclideanSpace ℝ n), |η.ofLp ⬝ᵥ (a x).mulVec ξ.ofLp| ≤ Lam * ‖η‖ * ‖ξ‖) (hb_bound : ∀ᵐ (x : α) ∂μ, ‖b x‖ ≤ beta) (hc_bound : ∀ᵐ (x : α) ∂μ, ‖c x‖ ≤ gamma) (hUV : MeasureTheory.Integrable (fun (x : α) => ‖U x‖ * ‖V x‖) μ) : MeasureTheory.Integrable (fun (x : α) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (V x)) μ

Bounded measurable coefficient fields and an integrable product of jet norms give an integrable scalar energy density.

theorem TauCeti.PDE.integrable_energyIntegrand_apply₂_of_memLp_two {α : Type u_1} {n : Type u_2} [MeasurableSpace α] [Fintype n] {μ : MeasureTheory.Measure α} {a : α → Matrix n n ℝ} {b : α → EuclideanSpace ℝ n} {c : α → ℝ} {U V : α → ℝ × EuclideanSpace ℝ n} {Lam beta gamma : ℝ} (hLam : 0 ≤ Lam) (ha : MeasureTheory.AEStronglyMeasurable a μ) (hb : MeasureTheory.AEStronglyMeasurable b μ) (hc : MeasureTheory.AEStronglyMeasurable c μ) (hU : MeasureTheory.MemLp U 2 μ) (hV : MeasureTheory.MemLp V 2 μ) (ha_bound : ∀ᵐ (x : α) ∂μ, ∀ (η ξ : EuclideanSpace ℝ n), |η.ofLp ⬝ᵥ (a x).mulVec ξ.ofLp| ≤ Lam * ‖η‖ * ‖ξ‖) (hb_bound : ∀ᵐ (x : α) ∂μ, ‖b x‖ ≤ beta) (hc_bound : ∀ᵐ (x : α) ∂μ, ‖c x‖ ≤ gamma) : MeasureTheory.Integrable (fun (x : α) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (V x)) μ

Bounded measurable coefficient fields and square-integrable jet fields give an integrable scalar energy density.

theorem TauCeti.PDE.integrable_energyIntegrand_apply₂_of_bounds {α : Type u_1} {n : Type u_2} [MeasurableSpace α] [Fintype n] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {a : α → Matrix n n ℝ} {b : α → EuclideanSpace ℝ n} {c : α → ℝ} {U V : α → ℝ × EuclideanSpace ℝ n} {Lam beta gamma R S : ℝ} (hLam : 0 ≤ Lam) (ha : MeasureTheory.AEStronglyMeasurable a μ) (hb : MeasureTheory.AEStronglyMeasurable b μ) (hc : MeasureTheory.AEStronglyMeasurable c μ) (hU : MeasureTheory.AEStronglyMeasurable U μ) (hV : MeasureTheory.AEStronglyMeasurable V μ) (ha_bound : ∀ᵐ (x : α) ∂μ, ∀ (η ξ : EuclideanSpace ℝ n), |η.ofLp ⬝ᵥ (a x).mulVec ξ.ofLp| ≤ Lam * ‖η‖ * ‖ξ‖) (hb_bound : ∀ᵐ (x : α) ∂μ, ‖b x‖ ≤ beta) (hc_bound : ∀ᵐ (x : α) ∂μ, ‖c x‖ ≤ gamma) (hU_bound : ∀ᵐ (x : α) ∂μ, ‖U x‖ ≤ R) (hV_bound : ∀ᵐ (x : α) ∂μ, ‖V x‖ ≤ S) : MeasureTheory.Integrable (fun (x : α) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (V x)) μ

Bounded measurable coefficient fields and bounded measurable jet fields give an integrable scalar energy density on a finite-measure space.

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

Fixed-jet specialization of integrable_energyIntegrand_apply₂_of_bounds.

theorem TauCeti.PDE.UniformlyEllipticOn.integrable_energyIntegrand_apply₂_of_integrable_norm_mul_on {α : Type u_1} {n : Type u_2} [MeasurableSpace α] [Fintype n] {μ : MeasureTheory.Measure α} {Ω : Set α} {a : α → Matrix n n ℝ} {b : α → EuclideanSpace ℝ n} {c : α → ℝ} {U V : α → ℝ × EuclideanSpace ℝ n} {lam Lam beta gamma : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) (hΩ : ∀ᵐ (x : α) ∂μ, x ∈ Ω) (ha : MeasureTheory.AEStronglyMeasurable a μ) (hb : MeasureTheory.AEStronglyMeasurable b μ) (hc : MeasureTheory.AEStronglyMeasurable c μ) (hU : MeasureTheory.AEStronglyMeasurable U μ) (hV : MeasureTheory.AEStronglyMeasurable V μ) (hb_bound : ∀ᵐ (x : α) ∂μ, ‖b x‖ ≤ beta) (hc_bound : ∀ᵐ (x : α) ∂μ, ‖c x‖ ≤ gamma) (hUV : MeasureTheory.Integrable (fun (x : α) => ‖U x‖ * ‖V x‖) μ) : MeasureTheory.Integrable (fun (x : α) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (V x)) μ

Uniform-ellipticity wrapper for scalar energy-density integrability.

If μ is a.e. supported on Ω, the named principal coefficient hypothesis UniformlyEllipticOn Ω a λ Λ supplies the a.e. bilinear upper bound required by integrable_energyIntegrand_apply₂_of_integrable_norm_mul.

theorem TauCeti.PDE.UniformlyEllipticOn.integrable_energyIntegrand_apply₂_of_memLp_two_on {α : Type u_1} {n : Type u_2} [MeasurableSpace α] [Fintype n] {μ : MeasureTheory.Measure α} {Ω : Set α} {a : α → Matrix n n ℝ} {b : α → EuclideanSpace ℝ n} {c : α → ℝ} {U V : α → ℝ × EuclideanSpace ℝ n} {lam Lam beta gamma : ℝ} (h : UniformlyEllipticOn Ω a lam Lam) (hΩ : ∀ᵐ (x : α) ∂μ, x ∈ Ω) (ha : MeasureTheory.AEStronglyMeasurable a μ) (hb : MeasureTheory.AEStronglyMeasurable b μ) (hc : MeasureTheory.AEStronglyMeasurable c μ) (hU : MeasureTheory.MemLp U 2 μ) (hV : MeasureTheory.MemLp V 2 μ) (hb_bound : ∀ᵐ (x : α) ∂μ, ‖b x‖ ≤ beta) (hc_bound : ∀ᵐ (x : α) ∂μ, ‖c x‖ ≤ gamma) : MeasureTheory.Integrable (fun (x : α) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (V x)) μ

Uniform-ellipticity wrapper for the square-integrable-jet energy-density criterion.

theorem TauCeti.PDE.UniformlyEllipticOn.integrable_energyIntegrand_apply₂_of_bounds_on {α : Type u_1} {n : Type u_2} [MeasurableSpace α] [Fintype n] {μ : MeasureTheory.Measure α} {Ω : Set α} {a : α → Matrix n n ℝ} {b : α → EuclideanSpace ℝ n} {c : α → ℝ} {U V : α → ℝ × EuclideanSpace ℝ n} {lam Lam beta gamma R S : ℝ} [MeasureTheory.IsFiniteMeasure μ] (h : UniformlyEllipticOn Ω a lam Lam) (hΩ : ∀ᵐ (x : α) ∂μ, x ∈ Ω) (ha : MeasureTheory.AEStronglyMeasurable a μ) (hb : MeasureTheory.AEStronglyMeasurable b μ) (hc : MeasureTheory.AEStronglyMeasurable c μ) (hU : MeasureTheory.AEStronglyMeasurable U μ) (hV : MeasureTheory.AEStronglyMeasurable V μ) (hb_bound : ∀ᵐ (x : α) ∂μ, ‖b x‖ ≤ beta) (hc_bound : ∀ᵐ (x : α) ∂μ, ‖c x‖ ≤ gamma) (hU_bound : ∀ᵐ (x : α) ∂μ, ‖U x‖ ≤ R) (hV_bound : ∀ᵐ (x : α) ∂μ, ‖V x‖ ≤ S) : MeasureTheory.Integrable (fun (x : α) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (V x)) μ

Uniform-ellipticity wrapper for bounded measurable jets on a finite-measure space.

theorem TauCeti.PDE.UniformlyEllipticOn.integrable_energyIntegrand_apply_of_bounds_on {α : Type u_1} {n : Type u_2} [MeasurableSpace α] [Fintype n] {μ : MeasureTheory.Measure α} {Ω : Set α} {a : α → Matrix n n ℝ} {b : α → EuclideanSpace ℝ n} {c : α → ℝ} {lam Lam beta gamma : ℝ} [MeasureTheory.IsFiniteMeasure μ] (h : UniformlyEllipticOn Ω a lam Lam) (hΩ : ∀ᵐ (x : α) ∂μ, x ∈ Ω) (ha : MeasureTheory.AEStronglyMeasurable a μ) (hb : MeasureTheory.AEStronglyMeasurable b μ) (hc : MeasureTheory.AEStronglyMeasurable c μ) (hb_bound : ∀ᵐ (x : α) ∂μ, ‖b x‖ ≤ beta) (hc_bound : ∀ᵐ (x : α) ∂μ, ‖c x‖ ≤ gamma) (U V : ℝ × EuclideanSpace ℝ n) : MeasureTheory.Integrable (fun (x : α) => ((energyIntegrand (a x) (b x) (c x)) U) V) μ

Fixed-jet specialization of UniformlyEllipticOn.integrable_energyIntegrand_apply₂_of_bounds_on.