The regularized forced curve with zero force

The measurable modification used by the forced construction may differ from zero on a null set. Its time slices therefore vanish almost everywhere, which identifies the resulting mild curve with the global zero-force curve.

theorem CKN.Leray.forcedZeroForceSlice_ae_eq_zero (T : ℝ) (hT : 0 < T) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), forcedForceSlice (forcedForceMod (fun (x : Foundation.Parabolic.ParabolicPoint) => 0) isLocallySquareIntegrableForce_zero) s = 0

The spatial L² force curve of a modification of zero vanishes for almost every positive time on each finite interval.

theorem CKN.Leray.forcedRegCurve_zero_eq_regularizedGlobalMildCurve (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (t : ℝ) : forcedRegCurve ρ ε hε ha isLocallySquareIntegrableForce_zero t = regularizedGlobalMildCurve ρ ε hε (forcedRegDatum ρ ε hε ha) ⋯ t

The forced construction with the zero force agrees with the global zero-force regularized mild curve.