Time increments of the regularized velocity

The pointwise time derivative of the regularized velocity (thm:regularised of the CKN manuscript, (R2)) and its slab square-integrability give the integrated increment of the velocity against a fixed L² test field, by Fubini's theorem (lem:lps-regularized-Hk-start).

theorem ESS.LPS.lps_scalar_test_pairing_interval_increment {f g : CKN.Foundation.Parabolic.Vec3 → ℝ → ℝ} {w : CKN.Foundation.Parabolic.Vec3 → ℝ} {a b : ℝ} (hab : a ≤ b) (hFcont : ∀ (x : CKN.Foundation.Parabolic.Vec3), ContinuousOn (fun (t : ℝ) => f x t) (Set.Icc a b)) (hGcont : ∀ (x : CKN.Foundation.Parabolic.Vec3), ContinuousOn (fun (t : ℝ) => g x t) (Set.Icc a b)) (hderiv : ∀ (x : CKN.Foundation.Parabolic.Vec3), ∀ t ∈ Set.Ioo a b, HasDerivAt (fun (s : ℝ) => f x s) (g x t) t) (hFa : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => f x a * w x) MeasureTheory.volume) (hFb : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => f x b * w x) MeasureTheory.volume) (hGprod : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z.1 z.2 * w z.1) ((MeasureTheory.volume.restrict Set.univ).prod (MeasureTheory.volume.restrict (Set.Ioc a b)))) : (∫ (x : CKN.Foundation.Parabolic.Vec3), f x b * w x) - ∫ (x : CKN.Foundation.Parabolic.Vec3), f x a * w x = ∫ (t : ℝ) in a..b, ∫ (x : CKN.Foundation.Parabolic.Vec3), g x t * w x

Pointwise time differentiation gives the integrated physical pairing increment after Fubini, for any fixed spatial test in the product space. This is the bridge from the regularized equation's pointwise derivatives to the derivative classes in physical L².

theorem ESS.LPS.lps_regR12_hasDerivAt_time (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) (z : CKN.Foundation.Parabolic.ParabolicPoint) : 0 < z.2 → ∀ (i : Fin 3), HasDerivAt (fun (s : ℝ) => CKN.Leray.regR12Velocity ρ ε hε b hb (z.1, s) i) (CKN.Leray.regR12TimeRHS ρ ε hε (CKN.Leray.regR12Velocity ρ ε hε b hb) (CKN.Leray.forcedQuadPressure ρ ε hε (CKN.Leray.regR12Curve ρ ε hε b hb)) z i) z.2

The regularized velocity has, at every positive time, the classical time derivative given by the regularized momentum right-hand side (lem:lps-regularized-Hk-start).

theorem ESS.LPS.lps_regR12_Q_facts (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) : (∀ (i : Fin 3), ContinuousOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Leray.regR12TimeRHS ρ ε hε (CKN.Leray.regR12Velocity ρ ε hε b hb) (CKN.Leray.forcedQuadPressure ρ ε hε (CKN.Leray.regR12Curve ρ ε hε b hb)) z i) (CKN.spaceTimeSet Set.univ (Set.Ioi 0))) ∧ ∀ (δ T : ℝ), 0 < δ → δ < T → ∀ (i : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Leray.regR12TimeRHS ρ ε hε (CKN.Leray.regR12Velocity ρ ε hε b hb) (CKN.Leray.forcedQuadPressure ρ ε hε (CKN.Leray.regR12Curve ρ ε hε b hb)) z i) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo δ T)))

The regularized momentum right-hand side is continuous on positive times and square-integrable on every positive-time slab (lem:lps-regularized-Hk-start).

theorem ESS.LPS.lps_pairing_increment_of_slab {f g : CKN.Foundation.Parabolic.Vec3 → ℝ → ℝ} {W : CKN.Foundation.Parabolic.Vec3 → ℝ} {a b : ℝ} (hab : a ≤ b) (hderiv : ∀ (x : CKN.Foundation.Parabolic.Vec3), ∀ t ∈ Set.Icc a b, HasDerivAt (f x) (g x t) t) (hgcont : ∀ (x : CKN.Foundation.Parabolic.Vec3), ContinuousOn (g x) (Set.Icc a b)) (hfa : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => f x a) 2 MeasureTheory.volume) (hfb : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => f x b) 2 MeasureTheory.volume) (hW : MeasureTheory.MemLp W 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z.1 z.2) 2 (MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioc a b))) : IntervalIntegrable (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), g x t * W x) MeasureTheory.volume a b ∧ (∫ (x : CKN.Foundation.Parabolic.Vec3), f x b * W x) - ∫ (x : CKN.Foundation.Parabolic.Vec3), f x a * W x = ∫ (t : ℝ) in a..b, ∫ (x : CKN.Foundation.Parabolic.Vec3), g x t * W x

Fubini form of the pairing increment: pointwise differentiability in time together with slab square-integrability of the derivative gives the integrated increment against a fixed L² test function.

theorem ESS.LPS.lps_regR12_time_pairing_increment (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {a c : ℝ} (ha : 0 < a) (hac : a ≤ c) (W : CKN.Foundation.Parabolic.Vec3 → ℝ) (hW : MeasureTheory.MemLp W 2 MeasureTheory.volume) (i : Fin 3) : IntervalIntegrable (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Leray.regR12TimeRHS ρ ε hε (CKN.Leray.regR12Velocity ρ ε hε b hb) (CKN.Leray.forcedQuadPressure ρ ε hε (CKN.Leray.regR12Curve ρ ε hε b hb)) (x, t) i * W x) MeasureTheory.volume a c ∧ (∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Leray.regR12Velocity ρ ε hε b hb (x, c) i * W x) - ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Leray.regR12Velocity ρ ε hε b hb (x, a) i * W x = ∫ (t : ℝ) in a..c, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Leray.regR12TimeRHS ρ ε hε (CKN.Leray.regR12Velocity ρ ε hε b hb) (CKN.Leray.forcedQuadPressure ρ ε hε (CKN.Leray.regR12Curve ρ ε hε b hb)) (x, t) i * W x

The pairing of the regularized velocity increment against a fixed L² test function equals the time integral of the pairing of the momentum right-hand side (lem:lps-regularized-Hk-start).