Squared norms of absolutely continuous families

A family of real functions of time, indexed by a spatial variable, that are absolutely continuous with a common square-integrable rate has an L² norm in the spatial variable that is absolutely continuous as well, with the expected derivative. This is the scalar time calculus behind the strong continuity and the energy identities of prop:lps-local-strong.

theorem ESS.LPS.lps_sq_integral_le {α : Type u_1} [MeasurableSpace α] {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure ν] {k : α → ℝ} (hk : MeasureTheory.Integrable k ν) (hk2 : MeasureTheory.Integrable (fun (x : α) => k x ^ 2) ν) : (∫ (x : α), k x ∂ν) ^ 2 ≤ ν.real Set.univ * ∫ (x : α), k x ^ 2 ∂ν

Cauchy–Schwarz for a finite measure in the form used for time integrals.

theorem ESS.LPS.lps_ac_sq_identity {a b : ℝ} (hab : a ≤ b) {F G : ℝ → ℝ} (hG : IntervalIntegrable G MeasureTheory.volume a b) (hF : ∀ s ∈ Set.Icc a b, ∀ t ∈ Set.Icc a b, F t - F s = ∫ (r : ℝ) in s..t, G r) (s : ℝ) : s ∈ Set.Icc a b → ∀ t ∈ Set.Icc a b, F t ^ 2 - F s ^ 2 = 2 * ∫ (r : ℝ) in s..t, F r * G r

A real function that is an interval integral of an integrable rate has squared increments given by the integral of 2 F G.

theorem ESS.LPS.lps_ac_family_sq_integrable {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.SFinite μ] {a b c : ℝ} (hab : a ≤ b) (hc : c ∈ Set.Icc a b) {f g : X → ℝ → ℝ} (hfm : Measurable fun (p : X × ℝ) => f p.1 p.2) (hgint : ∀ (x : X), IntervalIntegrable (g x) MeasureTheory.volume a b) (hAC : ∀ (x : X), ∀ s ∈ Set.Icc a b, ∀ t ∈ Set.Icc a b, f x t - f x s = ∫ (r : ℝ) in s..t, g x r) (hg2 : MeasureTheory.Integrable (fun (p : X × ℝ) => g p.1 p.2 ^ 2) (μ.prod (MeasureTheory.volume.restrict (Set.Ioc a b)))) (hfc : MeasureTheory.Integrable (fun (x : X) => f x c ^ 2) μ) : (∀ t ∈ Set.Icc a b, MeasureTheory.Integrable (fun (x : X) => f x t ^ 2) μ) ∧ MeasureTheory.Integrable (fun (p : X × ℝ) => f p.1 p.2 ^ 2) (μ.prod (MeasureTheory.volume.restrict (Set.Ioc a b)))

Slice and joint square integrability of an absolutely continuous family with square-integrable rate and a square-integrable slice at one time c.

theorem ESS.LPS.lps_ac_family_energy_identity {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.SFinite μ] {a b : ℝ} (hab : a ≤ b) {f g : X → ℝ → ℝ} (hfm : Measurable fun (p : X × ℝ) => f p.1 p.2) (hgm : Measurable fun (p : X × ℝ) => g p.1 p.2) (hgint : ∀ (x : X), IntervalIntegrable (g x) MeasureTheory.volume a b) (hAC : ∀ (x : X), ∀ s ∈ Set.Icc a b, ∀ t ∈ Set.Icc a b, f x t - f x s = ∫ (r : ℝ) in s..t, g x r) (hf2 : MeasureTheory.Integrable (fun (p : X × ℝ) => f p.1 p.2 ^ 2) (μ.prod (MeasureTheory.volume.restrict (Set.Ioc a b)))) (hg2 : MeasureTheory.Integrable (fun (p : X × ℝ) => g p.1 p.2 ^ 2) (μ.prod (MeasureTheory.volume.restrict (Set.Ioc a b)))) (hslice : ∀ t ∈ Set.Icc a b, MeasureTheory.Integrable (fun (x : X) => f x t ^ 2) μ) (s : ℝ) : s ∈ Set.Icc a b → ∀ t ∈ Set.Icc a b, s ≤ t → ∫ (x : X), f x t ^ 2 ∂μ - ∫ (x : X), f x s ^ 2 ∂μ = 2 * ∫ (r : ℝ) in s..t, ∫ (x : X), f x r * g x r ∂μ

The L² energy of an absolutely continuous family changes by the integral of the pairing of the family with its rate: this is the chain rule in time for ‖f(t)‖², in the spatial variable x, whenever the family and the rate are jointly square integrable.