Coordinate representatives of the interval mild path

The interval mild identity identifies each positive-time coordinate slice almost everywhere with the representative of its zero-force construction.

theorem CKN.Leray.regularisedInterval_velocity_ae_eq_forcedRegRep (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (T : ℝ) (hT : 0 < T) (hSlice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hL2Continuous : Continuous fun (t : ↑(Set.Icc 0 T)) => realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, ↑t)) ⋯) (hMild : ∀ (t : ℝ) (ht : t ∈ Set.Icc 0 T), realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) ⋯ = realHeatOperator t ⋯ (realVectorL2OfCoordinateFunction (regUniformMollifiedInitial ρ ε hε a) ⋯) - regularizedMildStokesIntegral (regularizedMildTensorTrajectory ρ ε hε (regularisedIntervalMildCurve u T ⋯ hSlice)) t) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) =ᵐ[MeasureTheory.volume] fun (x : Foundation.Parabolic.Vec3) => forcedRegRep ρ ε hε ha isLocallySquareIntegrableForce_zero (x, t)

The coordinate velocity of an interval mild path agrees almost everywhere on each slice with the representative of its forced zero-force curve.