The space-time energy identity of the mollified velocity

Integrating the time energy identity of the mollified forced regularized velocity over all spatial points and exchanging the order of integration gives ∫∫ w² ∂ₜψ = 2 ∫∫ w S ψ on a bounded slab, for every smooth compactly supported space-time test ψ. The exchanges are justified by joint measurability and the uniform bounds of the mollified velocity and of its source. This is the time part of eq:reg-local-energy-forced.

theorem CKN.Leray.ae_prod_of_ae_forall {P : Foundation.Parabolic.Vec3 × ℝ → Prop} {ν : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite ν] (h : ∀ᵐ (t : ℝ) ∂ν, ∀ (x : Foundation.Parabolic.Vec3), P (x, t)) : ∀ᵐ (z : Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.prod ν, P z

A property holding for almost every time and every point holds almost everywhere on the product.

theorem CKN.Leray.stronglyMeasurable_leW (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {η : Foundation.Parabolic.Vec3 → ℝ} (hη : Continuous η) (k : Fin 3) : MeasureTheory.StronglyMeasurable fun (p : Foundation.Parabolic.Vec3 × ℝ) => leW ρ ε hε ha hf η p.1 p.2 k

theorem CKN.Leray.stronglyMeasurable_leSF (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {η : Foundation.Parabolic.Vec3 → ℝ} (hη : ContDiff ℝ (↑⊤) η) (k : Fin 3) : MeasureTheory.StronglyMeasurable fun (p : Foundation.Parabolic.Vec3 × ℝ) => leSF ρ ε hε ha hf η p.1 p.2 k

theorem CKN.Leray.forcedRegRep_slice_bound (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (T : ℝ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ t ∈ Set.Icc 0 T, ∀ (k : Fin 3), (MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => forcedRegRep ρ ε hε ha hf (y, t) k) 2 MeasureTheory.volume).toReal ≤ C

theorem CKN.Leray.abs_leW_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {η : Foundation.Parabolic.Vec3 → ℝ} (hη : Continuous η) (hηc : HasCompactSupport η) (x : Foundation.Parabolic.Vec3) (t : ℝ) (k : Fin 3) : |leW ρ ε hε ha hf η x t k| ≤ (MeasureTheory.eLpNorm η 2 MeasureTheory.volume).toReal * (MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => forcedRegRep ρ ε hε ha hf (y, t) k) 2 MeasureTheory.volume).toReal

theorem CKN.Leray.ae_abs_leSF_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {η : Foundation.Parabolic.Vec3 → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (k : Fin 3) {T : ℝ} (hT : 0 < T) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ (x : Foundation.Parabolic.Vec3), |leSF ρ ε hε ha hf η x t k| ≤ leSourceBound ρ ε hε ha hf η k t

theorem CKN.Leray.timePartial_eq_fderiv {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (z : Foundation.Parabolic.Vec3 × ℝ) : timePartial ψ z = (fderiv ℝ ψ z) (0, 1)

theorem CKN.Leray.integrable_timePartial_prod {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (T : ℝ) : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => timePartial ψ z) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

theorem CKN.Leray.integral_leW_sq_spaceTime (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {η : Foundation.Parabolic.Vec3 → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (k : Fin 3) {T : ℝ} (hT : 0 < T) {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) {c d : ℝ} (hc : 0 < c) (hcd : c < d) (hdT : d < T) (hψs : ∀ z ∈ tsupport ψ, z.2 ∈ Set.Ioo c d) : ∫ (t : ℝ) in Set.Ioo 0 T, ∫ (x : Foundation.Parabolic.Vec3), leW ρ ε hε ha hf η x t k ^ 2 * timePartial ψ (x, t) = 2 * ∫ (t : ℝ) in Set.Ioo 0 T, ∫ (x : Foundation.Parabolic.Vec3), leW ρ ε hε ha hf η x t k * leSF ρ ε hε ha hf η x t k * ψ (x, t)

The space-time energy identity of the mollified velocity.