Continuous L² curves for a field and its first gradient

A scalar slab field with square-integrable time derivative has a continuous L²-valued representative, and its weak spatial derivative, if it has a square-integrable weak spatial derivative, has one too, with the energy identities of prop:lps-local-strong.

theorem ESS.LPS.lps_vlMoll_slab_tendsto {a b : ℝ} {g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hgm : MeasureTheory.StronglyMeasurable g) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, (CKN.vlConvT (CKN.vlMoll n) g z.1 z.2 - g z) ^ 2) Filter.atTop (nhds 0)

Mollifier convergence on a slab, in slab-integral form.

theorem ESS.LPS.lps_l2_time_curve {a b : ℝ} {w r : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hab : a < b) (hwm : MeasureTheory.StronglyMeasurable w) (hrm : MeasureTheory.StronglyMeasurable r) (hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hr : MeasureTheory.MemLp r 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hweak : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, w p * CKN.timePartial φ p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, r p * φ p) : ∃ (L : ↑(Set.Icc a b) → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)), Continuous L ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ (hs : s ∈ Set.Icc a b), ↑↑(L ⟨s, hs⟩) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => w (x, s)) ∧ ∀ (s t : ℝ) (hs : s ∈ Set.Icc a b) (ht : t ∈ Set.Icc a b), s ≤ t → ‖L ⟨t, ht⟩‖ ^ 2 - ‖L ⟨s, hs⟩‖ ^ 2 = 2 * ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab s t, w z * r z

The field itself: a continuous L² curve and its energy identity.

theorem ESS.LPS.lps_conv_second_deriv_ae {a b : ℝ} {w g h : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (j : Fin 3) (hwm : MeasureTheory.StronglyMeasurable w) (hhm : MeasureTheory.StronglyMeasurable h) (hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hh : MeasureTheory.MemLp h 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hgrad : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, w p * CKN.spatialPartial φ j p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, g p * φ p) (hhess : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, g p * CKN.spatialPartial φ j p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, h p * φ p) {κ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hκ : CKN.IsVlKernel κ) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConvT (CKN.vlDeriv (CKN.vlDeriv κ j) j) w x s = CKN.vlConvT κ h x s

Second spatial derivative of a slab field as an identity between kernel convolutions, for almost every time and almost every point.

theorem ESS.LPS.lps_conv_first_deriv_ae {a b : ℝ} {w g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (j : Fin 3) (hwm : MeasureTheory.StronglyMeasurable w) (hgm : MeasureTheory.StronglyMeasurable g) (hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hgrad : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, w p * CKN.spatialPartial φ j p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, g p * φ p) {κ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hκ : CKN.IsVlKernel κ) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConvT (CKN.vlDeriv κ j) w x s = CKN.vlConvT κ g x s

First spatial derivative of a slab field as an identity between kernel convolutions, for almost every time and almost every point.

theorem ESS.LPS.lps_grad_pairing {a b : ℝ} {w r g h : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (j : Fin 3) (hwm : MeasureTheory.StronglyMeasurable w) (hrm : MeasureTheory.StronglyMeasurable r) (hhm : MeasureTheory.StronglyMeasurable h) (hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hr : MeasureTheory.MemLp r 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hh : MeasureTheory.MemLp h 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hgrad : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, w p * CKN.spatialPartial φ j p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, g p * φ p) (hhess : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, g p * CKN.spatialPartial φ j p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, h p * φ p) {κ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hκ : CKN.IsVlKernel κ) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConvT (CKN.vlDeriv κ j) w x s * CKN.vlConvT (CKN.vlDeriv κ j) r x s = -∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConvT κ h x s * CKN.vlConvT κ r x s

The slice pairing of the differentiated convolutions is minus the pairing of the convolved second derivative with the convolved time derivative.

theorem ESS.LPS.lps_slab_sq_congr {a b : ℝ} {F G g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hG : MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hFG : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), F (x, s) = G (x, s)) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, (F z - g z) ^ 2 = ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, (G z - g z) ^ 2

Almost everywhere agreement on almost every slice gives equal slab distances to a common field.

theorem ESS.LPS.lps_gradient_time_curve {a b : ℝ} {w r g h : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hab : a < b) (j : Fin 3) (hwm : MeasureTheory.StronglyMeasurable w) (hrm : MeasureTheory.StronglyMeasurable r) (hgm : MeasureTheory.StronglyMeasurable g) (hhm : MeasureTheory.StronglyMeasurable h) (hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hr : MeasureTheory.MemLp r 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hh : MeasureTheory.MemLp h 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hweak : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, w p * CKN.timePartial φ p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, r p * φ p) (hgrad : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, w p * CKN.spatialPartial φ j p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, g p * φ p) (hhess : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, g p * CKN.spatialPartial φ j p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, h p * φ p) : ∃ (L : ↑(Set.Icc a b) → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)), Continuous L ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ (hs : s ∈ Set.Icc a b), ↑↑(L ⟨s, hs⟩) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, s)) ∧ ∀ (s t : ℝ) (hs : s ∈ Set.Icc a b) (ht : t ∈ Set.Icc a b), s ≤ t → ‖L ⟨t, ht⟩‖ ^ 2 - ‖L ⟨s, hs⟩‖ ^ 2 = -(2 * ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab s t, h z * r z)

The first spatial gradient: a continuous L² curve and its energy identity, in direction j.