Identification of an interval mild path

The same-velocity mild identity identifies the interval path with the zero-force forced construction on that interval.

theorem CKN.Leray.regularisedIntervalMildCurve_eq_forcedRegCurve (ρ : 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) : regularisedIntervalMildCurve u T ⋯ hSlice t = forcedRegCurve ρ ε hε ha isLocallySquareIntegrableForce_zero t

A coordinate field satisfying the same-velocity mild identity has the zero-force forced regularized curve as its spatial L² path.