Measurability of pointwise PDE energy integrands

The weak-form lane of the PDE roadmap is stated for bounded measurable coefficients. Before the pointwise jet integrand x ↦ energyIntegrand (a x) (b x) (c x) can be integrated over a domain, it must be available as a strongly measurable field of continuous bilinear forms, and its scalar evaluations on measurable jet fields must be a.e. strongly measurable.

This file supplies that finite-dimensional bookkeeping. It does not introduce a bundled bounded-measurable-coefficient predicate; coefficient regularity remains stated inline, following the roadmap and Mathlib style.

Main declarations

• stronglyMeasurable_energyIntegrand and aestronglyMeasurable_energyIntegrand: measurable coefficient fields give a measurable field of pointwise energy integrands.
• stronglyMeasurable_energyIntegrand_apply, stronglyMeasurable_energyIntegrand_apply₂, aestronglyMeasurable_energyIntegrand_apply, and aestronglyMeasurable_energyIntegrand_apply₂: scalar evaluations on fixed or measurable jet fields are measurable.

theorem TauCeti.PDE.stronglyMeasurable_energyIntegrand {α : Type u_1} {n : Type u_2} [MeasurableSpace α] [Fintype n] {a : α → Matrix n n ℝ} {b : α → EuclideanSpace ℝ n} {c : α → ℝ} (ha : MeasureTheory.StronglyMeasurable a) (hb : MeasureTheory.StronglyMeasurable b) (hc : MeasureTheory.StronglyMeasurable c) : MeasureTheory.StronglyMeasurable fun (x : α) => energyIntegrand (a x) (b x) (c x)

Strongly measurable coefficient fields give a strongly measurable field of pointwise energy integrands.

theorem TauCeti.PDE.stronglyMeasurable_energyIntegrand_apply₂ {α : Type u_1} {n : Type u_2} [MeasurableSpace α] [Fintype n] {a : α → Matrix n n ℝ} {b : α → EuclideanSpace ℝ n} {c : α → ℝ} {U V : α → ℝ × EuclideanSpace ℝ n} (ha : MeasureTheory.StronglyMeasurable a) (hb : MeasureTheory.StronglyMeasurable b) (hc : MeasureTheory.StronglyMeasurable c) (hU : MeasureTheory.StronglyMeasurable U) (hV : MeasureTheory.StronglyMeasurable V) : MeasureTheory.StronglyMeasurable fun (x : α) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (V x)

Strongly measurable coefficient fields and strongly measurable jet fields give a strongly measurable scalar energy density.

theorem TauCeti.PDE.stronglyMeasurable_energyIntegrand_apply {α : Type u_1} {n : Type u_2} [MeasurableSpace α] [Fintype n] {a : α → Matrix n n ℝ} {b : α → EuclideanSpace ℝ n} {c : α → ℝ} (ha : MeasureTheory.StronglyMeasurable a) (hb : MeasureTheory.StronglyMeasurable b) (hc : MeasureTheory.StronglyMeasurable c) (U V : ℝ × EuclideanSpace ℝ n) : MeasureTheory.StronglyMeasurable fun (x : α) => ((energyIntegrand (a x) (b x) (c x)) U) V

Strongly measurable coefficient fields give strongly measurable scalar evaluations of the pointwise energy integrand on fixed jets.

theorem TauCeti.PDE.aestronglyMeasurable_energyIntegrand {α : Type u_1} {n : Type u_2} [MeasurableSpace α] [Fintype n] {μ : MeasureTheory.Measure α} {a : α → Matrix n n ℝ} {b : α → EuclideanSpace ℝ n} {c : α → ℝ} (ha : MeasureTheory.AEStronglyMeasurable a μ) (hb : MeasureTheory.AEStronglyMeasurable b μ) (hc : MeasureTheory.AEStronglyMeasurable c μ) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => energyIntegrand (a x) (b x) (c x)) μ

A.e. strongly measurable coefficient fields give an a.e. strongly measurable field of pointwise energy integrands.

theorem TauCeti.PDE.aestronglyMeasurable_energyIntegrand_apply {α : Type u_1} {n : Type u_2} [MeasurableSpace α] [Fintype n] {μ : MeasureTheory.Measure α} {a : α → Matrix n n ℝ} {b : α → EuclideanSpace ℝ n} {c : α → ℝ} (ha : MeasureTheory.AEStronglyMeasurable a μ) (hb : MeasureTheory.AEStronglyMeasurable b μ) (hc : MeasureTheory.AEStronglyMeasurable c μ) (U V : ℝ × EuclideanSpace ℝ n) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => ((energyIntegrand (a x) (b x) (c x)) U) V) μ

A.e. strongly measurable coefficient fields give a.e. strongly measurable scalar evaluations of the pointwise energy integrand on fixed jets.

theorem TauCeti.PDE.aestronglyMeasurable_energyIntegrand_apply₂ {α : Type u_1} {n : Type u_2} [MeasurableSpace α] [Fintype n] {μ : MeasureTheory.Measure α} {a : α → Matrix n n ℝ} {b : α → EuclideanSpace ℝ n} {c : α → ℝ} {U V : α → ℝ × EuclideanSpace ℝ n} (ha : MeasureTheory.AEStronglyMeasurable a μ) (hb : MeasureTheory.AEStronglyMeasurable b μ) (hc : MeasureTheory.AEStronglyMeasurable c μ) (hU : MeasureTheory.AEStronglyMeasurable U μ) (hV : MeasureTheory.AEStronglyMeasurable V μ) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => ((energyIntegrand (a x) (b x) (c x)) (U x)) (V x)) μ

A.e. strongly measurable coefficient fields and a.e. strongly measurable jet fields give an a.e. strongly measurable scalar energy density.