Time regularity of a field with square-integrable derivatives

The continuous L² curves of a field and of its first gradient, for fields that are only almost everywhere strongly measurable (prop:lps-local-strong).

theorem ESS.LPS.lps_slab_ae_slice {a b : ℝ} {f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : f =ᵐ[MeasureTheory.volume.restrict (CKN.vlSlab a b)] g) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, s)) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, s)

Almost everywhere equality on a slab gives almost everywhere equality of almost every time slice.

theorem ESS.LPS.lps_slab_integral_mul_congr {a b : ℝ} {f f' t : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : f =ᵐ[MeasureTheory.volume.restrict (CKN.vlSlab a b)] f') : ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, f p * t p = ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, f' p * t p

Almost everywhere equal factors give equal slab integrals against a fixed weight.

theorem ESS.LPS.lps_l2_time_curve_ae {a b : ℝ} {w r : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hab : a < b) (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, for a field that is only almost everywhere strongly measurable.

theorem ESS.LPS.lps_gradient_time_curve_ae {a b : ℝ} {w r g h : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hab : a < b) (j : Fin 3) (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 specified first gradient, for fields that are only almost everywhere strongly measurable.

theorem ESS.LPS.lps_strong_time_regularity {t₀ T : ℝ} (hT : t₀ < T) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hDerivs : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ T) u Du D2u Dtu) (hMemU : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hMemDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hMemD2u : MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hMemDtu : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) : ∃ (Lu : Fin 3 → ↑(Set.Icc t₀ T) → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) (LD : Fin 3 → Fin 3 → ↑(Set.Icc t₀ T) → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)), (∀ (i : Fin 3), Continuous (Lu i)) ∧ (∀ (i j : Fin 3), Continuous (LD i j)) ∧ (∀ (i : Fin 3), ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo t₀ T), ∀ (hs : s ∈ Set.Icc t₀ T), ↑↑(Lu i ⟨s, hs⟩) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s) i) ∧ (∀ (i j : Fin 3), ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo t₀ T), ∀ (hs : s ∈ Set.Icc t₀ T), ↑↑(LD i j ⟨s, hs⟩) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => Du (x, s) i j) ∧ (∀ (s t : ℝ) (hs : s ∈ Set.Icc t₀ T) (ht : t ∈ Set.Icc t₀ T), s ≤ t → ∑ i : Fin 3, (‖Lu i ⟨t, ht⟩‖ ^ 2 - ‖Lu i ⟨s, hs⟩‖ ^ 2) = 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo s t), ∑ i : Fin 3, u z i * Dtu z i) ∧ ∀ (s t : ℝ) (hs : s ∈ Set.Icc t₀ T) (ht : t ∈ Set.Icc t₀ T), s ≤ t → ∑ i : Fin 3, ∑ j : Fin 3, (‖LD i j ⟨t, ht⟩‖ ^ 2 - ‖LD i j ⟨s, hs⟩‖ ^ 2) = -(2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo s t), ∑ i : Fin 3, Dtu z i * ∑ j : Fin 3, D2u z i j j)

Time regularity of a field, its first gradient, second gradient and time derivative that are square integrable on a slab with the space-time weak derivative relations: continuous L² representatives with the energy identities (prop:lps-local-strong).