Variable-coefficient energy forms on L² jets

A divergence-form operator with bounded coefficients has an associated bounded bilinear form, its energy form. TauCeti.Analysis.PDE.EnergyForm.Lp treats constant coefficients; this file supplies the variable-coefficient construction. An essentially bounded field of pointwise continuous bilinear forms acts by Hölder multiplication

L∞(X; J →L J →L ℝ) × L²(X; J) → L²(X; J →L ℝ),

and the result pairs with a second L² jet. Both operations are Mathlib's ContinuousLinearMap.holderL and ContinuousLinearMap.lpPairing.

For PDE coefficients a, b, and c, the pointwise form is energyIntegrand (a x) (b x) (c x). Requiring this field to belong to L∞ is the precise boundedness and measurability hypothesis needed by the construction. The resulting form is bundled and continuous, so later Sobolev value-gradient jets can feed it without carrying integrability proofs at each use site.

Main declarations

• TauCeti.PDE.energyFormLpVariable: the variable-coefficient divergence-form energy form.
• TauCeti.PDE.energyFormLpVariable_apply: its characterization by the expected energy integral.

No formal source is vendored. The construction directly composes Mathlib's Hölder map and Lᵖ pairing from Mathlib.MeasureTheory.Function.Holder.

noncomputable def TauCeti.PDE.energyFormLpVariable {X : Type u_1} [MeasurableSpace X] {n : Type u_2} [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (hcoeff : MeasureTheory.MemLp (fun (x : X) => energyIntegrand (a x) (b x) (c x)) ⊤ μ) : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ) →L[ℝ] ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ) →L[ℝ] ℝ

The variable-coefficient divergence-form energy form on square-integrable value-gradient jets.

The MemLp ... ⊤ μ argument records exactly that the pointwise energy forms are strongly measurable and essentially bounded. Its proof is irrelevant to the resulting form.

Equations

• TauCeti.PDE.energyFormLpVariable μ a b c hcoeff = TauCeti.lpBilinearForm μ (MeasureTheory.MemLp.toLp (fun (x : X) => TauCeti.PDE.energyIntegrand (a x) (b x) (c x)) hcoeff)

@[simp]

theorem TauCeti.PDE.energyFormLpVariable_apply {X : Type u_1} [MeasurableSpace X] {n : Type u_2} [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (hcoeff : MeasureTheory.MemLp (fun (x : X) => energyIntegrand (a x) (b x) (c x)) ⊤ μ) (U V : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ)) : ((energyFormLpVariable μ a b c hcoeff) U) V = ∫ (x : X), ((energyIntegrand (a x) (b x) (c x)) (↑↑U x)) (↑↑V x) ∂μ

The variable-coefficient L² energy form is the integral of the pointwise jet energy density.

theorem TauCeti.PDE.energyFormLpVariable_proof_irrel {X : Type u_1} [MeasurableSpace X] {n : Type u_2} [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (hcoeff hcoeff' : MeasureTheory.MemLp (fun (x : X) => energyIntegrand (a x) (b x) (c x)) ⊤ μ) : energyFormLpVariable μ a b c hcoeff = energyFormLpVariable μ a b c hcoeff'

The variable-coefficient energy form is independent of the proof that its coefficient field belongs to L∞.

theorem TauCeti.PDE.energyFormLpVariable_congr_ae {X : Type u_1} [MeasurableSpace X] {n : Type u_2} [Fintype n] {μ : MeasureTheory.Measure X} {a a' : X → Matrix n n ℝ} {b b' : X → EuclideanSpace ℝ n} {c c' : X → ℝ} (ha : a =ᵐ[μ] a') (hb : b =ᵐ[μ] b') (hc : c =ᵐ[μ] c') (hcoeff : MeasureTheory.MemLp (fun (x : X) => energyIntegrand (a x) (b x) (c x)) ⊤ μ) (hcoeff' : MeasureTheory.MemLp (fun (x : X) => energyIntegrand (a' x) (b' x) (c' x)) ⊤ μ) : energyFormLpVariable μ a b c hcoeff = energyFormLpVariable μ a' b' c' hcoeff'

Almost-everywhere equal coefficient fields induce the same variable-coefficient energy form.

theorem TauCeti.PDE.energyFormLpVariable_zero_drift_transpose_apply {X : Type u_1} [MeasurableSpace X] {n : Type u_2} [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (c : X → ℝ) (hcoeff : MeasureTheory.MemLp (fun (x : X) => energyIntegrand (a x).transpose 0 (c x)) ⊤ μ) (hcoeff' : MeasureTheory.MemLp (fun (x : X) => energyIntegrand (a x) 0 (c x)) ⊤ μ) (U V : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ)) : ((energyFormLpVariable μ (fun (x : X) => (a x).transpose) (fun (x : X) => 0) c hcoeff) U) V = ((energyFormLpVariable μ a (fun (x : X) => 0) c hcoeff') V) U

Transposing the principal coefficient swaps the arguments of a variable zero-drift energy form.

theorem TauCeti.PDE.energyFormLpVariable_zero_drift_comm_of_isSymm_ae {X : Type u_1} [MeasurableSpace X] {n : Type u_2} [Fintype n] {μ : MeasureTheory.Measure X} {a : X → Matrix n n ℝ} (ha : ∀ᵐ (x : X) ∂μ, (a x).IsSymm) (c : X → ℝ) (hcoeff : MeasureTheory.MemLp (fun (x : X) => energyIntegrand (a x) 0 (c x)) ⊤ μ) (U V : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ)) : ((energyFormLpVariable μ a (fun (x : X) => 0) c hcoeff) U) V = ((energyFormLpVariable μ a (fun (x : X) => 0) c hcoeff) V) U

An a.e. symmetric principal coefficient gives a symmetric variable zero-drift energy form.

@[simp]

theorem TauCeti.PDE.energyFormLpVariable_zero_drift_flip_eq_of_isSymm_ae {X : Type u_1} [MeasurableSpace X] {n : Type u_2} [Fintype n] {μ : MeasureTheory.Measure X} {a : X → Matrix n n ℝ} (ha : ∀ᵐ (x : X) ∂μ, (a x).IsSymm) (c : X → ℝ) (hcoeff : MeasureTheory.MemLp (fun (x : X) => energyIntegrand (a x) 0 (c x)) ⊤ μ) : (energyFormLpVariable μ a (fun (x : X) => 0) c hcoeff).flip = energyFormLpVariable μ a (fun (x : X) => 0) c hcoeff

An a.e. symmetric principal coefficient makes the variable zero-drift energy form equal to its flip.

theorem TauCeti.PDE.energyFormLpVariable_coefficientSymmetricPart_self {X : Type u_1} [MeasurableSpace X] {n : Type u_2} [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (b : X → EuclideanSpace ℝ n) (c : X → ℝ) (hcoeff : MeasureTheory.MemLp (fun (x : X) => energyIntegrand (coefficientSymmetricPart (a x)) (b x) (c x)) ⊤ μ) (hcoeff' : MeasureTheory.MemLp (fun (x : X) => energyIntegrand (a x) (b x) (c x)) ⊤ μ) (U : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ)) : ((energyFormLpVariable μ (fun (x : X) => coefficientSymmetricPart (a x)) b c hcoeff) U) U = ((energyFormLpVariable μ a b c hcoeff') U) U

Replacing the principal coefficient by its symmetric part does not change the diagonal variable energy form.

theorem TauCeti.PDE.energyFormLpVariable_coefficientSymmetricPart_zero_drift_apply {X : Type u_1} [MeasurableSpace X] {n : Type u_2} [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (c : X → ℝ) (hsymm : MeasureTheory.MemLp (fun (x : X) => energyIntegrand (coefficientSymmetricPart (a x)) 0 (c x)) ⊤ μ) (hcoeff : MeasureTheory.MemLp (fun (x : X) => energyIntegrand (a x) 0 (c x)) ⊤ μ) (U V : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ)) : ((energyFormLpVariable μ (fun (x : X) => coefficientSymmetricPart (a x)) (fun (x : X) => 0) c hsymm) U) V = (((energyFormLpVariable μ a (fun (x : X) => 0) c hcoeff) U) V + ((energyFormLpVariable μ a (fun (x : X) => 0) c hcoeff) V) U) / 2

The symmetric-part variable zero-drift energy form is the average of the original form and its transpose.

theorem TauCeti.PDE.energyFormLpVariable_coefficientSymmetricPart_zero_drift_comm {X : Type u_1} [MeasurableSpace X] {n : Type u_2} [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (c : X → ℝ) (hcoeff : MeasureTheory.MemLp (fun (x : X) => energyIntegrand (coefficientSymmetricPart (a x)) 0 (c x)) ⊤ μ) (U V : ↥(MeasureTheory.Lp (ℝ × EuclideanSpace ℝ n) 2 μ)) : ((energyFormLpVariable μ (fun (x : X) => coefficientSymmetricPart (a x)) (fun (x : X) => 0) c hcoeff) U) V = ((energyFormLpVariable μ (fun (x : X) => coefficientSymmetricPart (a x)) (fun (x : X) => 0) c hcoeff) V) U

The symmetric-part variable zero-drift energy form is symmetric.

@[simp]

theorem TauCeti.PDE.energyFormLpVariable_coefficientSymmetricPart_zero_drift_flip_eq {X : Type u_1} [MeasurableSpace X] {n : Type u_2} [Fintype n] (μ : MeasureTheory.Measure X) (a : X → Matrix n n ℝ) (c : X → ℝ) (hcoeff : MeasureTheory.MemLp (fun (x : X) => energyIntegrand (coefficientSymmetricPart (a x)) 0 (c x)) ⊤ μ) : (energyFormLpVariable μ (fun (x : X) => coefficientSymmetricPart (a x)) (fun (x : X) => 0) c hcoeff).flip = energyFormLpVariable μ (fun (x : X) => coefficientSymmetricPart (a x)) (fun (x : X) => 0) c hcoeff

The symmetric-part variable zero-drift energy form is equal to its flip.