Time increments of L²-continuous fields with an L² time derivative

prop:lps-smoothing: a field u on the slab ℝ³ × (t₀, T) that is continuous into L² on [t₀, T] and whose weak time derivative ∂ₜu is square integrable on the slab satisfies, for every smooth compactly supported spatial test ψ, the pairing identity ⟨u(t) - u(s), ψ⟩ = ∫ₛᵗ ⟨∂ₜu(τ), ψ⟩ dτ, and the increment bound ‖u(t) - u(s)‖² ≤ (t - s) ∫ₛᵗ ‖∂ₜu(τ)‖² dτ.

theorem ESS.lps_slice_pairing_sub_eq_integral {t₀ T : ℝ} (hT : t₀ < T) {u Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hDt : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (htime : ∀ (i : Fin 3), ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo t₀ T), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T), u z i * CKN.timePartial φ z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T), Dtu z i * φ z) (hslice : ∀ t ∈ Set.Icc t₀ T, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hcont : ∀ t ∈ Set.Icc t₀ T, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s) - u (x, t)) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc t₀ T)) (nhds 0)) {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (i : Fin 3) {s t : ℝ} (hs : t₀ ≤ s) (hst : s ≤ t) (ht : t ≤ T) : (∫ (x : CKN.Foundation.Parabolic.Vec3), u (x, t) i * ψ x) - ∫ (x : CKN.Foundation.Parabolic.Vec3), u (x, s) i * ψ x = ∫ (τ : ℝ) in s..t, ∫ (x : CKN.Foundation.Parabolic.Vec3), Dtu (x, τ) i * ψ x

prop:lps-smoothing: for a field continuous into L² on [t₀, T] with a square-integrable weak time derivative on the slab, the spatial pairing of each component with a smooth compactly supported test changes between two times by the time integral of the paired derivative.

theorem ESS.lps_integral_sq_le_of_test_pairing_le {w : CKN.Foundation.Parabolic.Vec3 → ℝ} (hw : MeasureTheory.MemLp w 2 MeasureTheory.volume) {M : ℝ} (hM : 0 ≤ M) (hbound : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → |∫ (x : CKN.Foundation.Parabolic.Vec3), w x * ψ x| ≤ M * √(∫ (x : CKN.Foundation.Parabolic.Vec3), ψ x ^ 2)) : ∫ (x : CKN.Foundation.Parabolic.Vec3), w x ^ 2 ≤ M ^ 2

Duality in L²: a square-integrable function whose pairings with smooth compactly supported tests are bounded by M times the L² norm of the test has squared L² norm at most M² (prop:lps-smoothing).

theorem ESS.lps_slice_increment_sq_le {t₀ T : ℝ} (hT : t₀ < T) {u Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hDt : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (htime : ∀ (i : Fin 3), ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo t₀ T), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T), u z i * CKN.timePartial φ z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T), Dtu z i * φ z) (hslice : ∀ t ∈ Set.Icc t₀ T, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hcont : ∀ t ∈ Set.Icc t₀ T, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s) - u (x, t)) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc t₀ T)) (nhds 0)) {s t : ℝ} (hs : t₀ ≤ s) (hst : s ≤ t) (ht : t ≤ T) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (u (x, t) i - u (x, s) i) ^ 2 ≤ (t - s) * ∫ (τ : ℝ) in s..t, ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, Dtu (x, τ) i ^ 2

prop:lps-smoothing: for a field continuous into L² on [t₀, T] with a square-integrable weak time derivative on the slab, the squared L² norm of an increment is at most the length of the time interval times the time integral of the squared L² norm of the time derivative.

theorem ESS.lps_slice_pairing_ae_tendsto_slope {t₀ T : ℝ} (hT : t₀ < T) {u Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hDt : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (htime : ∀ (i : Fin 3), ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo t₀ T), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T), u z i * CKN.timePartial φ z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T), Dtu z i * φ z) (hslice : ∀ t ∈ Set.Icc t₀ T, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hcont : ∀ t ∈ Set.Icc t₀ T, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s) - u (x, t)) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc t₀ T)) (nhds 0)) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo t₀ T), ∀ (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∀ (i : Fin 3), Filter.Tendsto (fun (h : ℝ) => 1 / h * ((∫ (x : CKN.Foundation.Parabolic.Vec3), u (x, t + h) i * ψ x) - ∫ (x : CKN.Foundation.Parabolic.Vec3), u (x, t) i * ψ x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (x : CKN.Foundation.Parabolic.Vec3), Dtu (x, t) i * ψ x))

prop:lps-smoothing: for a field continuous into L² on [t₀, T] with a square-integrable weak time derivative on the slab, almost every time of (t₀, T) is a Lebesgue point of every spatial pairing: the forward difference quotients of the pairing of each component with any smooth compactly supported test converge to the pairing of the time derivative.