Uniqueness for the interval regularized mild identity

An interval mild path with the prescribed mollified initial state agrees with the zero-force global mild curve on that interval.

theorem CKN.Leray.regularizedMildIntervalPath_eq_global (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (hb : RegularizedMildJData b) (T : ℝ) (hT : 0 ≤ T) (U : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (hU : IsRegularizedMildTrajectory ρ ε hε b T U) (t : ↑(RegularizedMildTimeInterval T)) : U t = regularizedGlobalMildCurve ρ ε hε b hb ↑t

Uniqueness identifies a same-velocity mild path on a closed finite interval with the global zero-force regularized curve.

theorem CKN.Leray.regularizedMildIntervalField_slice_eq_global (ρ : 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ε fun (s : ℝ) => realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, ↑(regularizedMildTimeClamp T hT s))) ⋯) t) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) ⋯ = regularizedGlobalMildCurve ρ ε hε (realVectorL2OfCoordinateFunction (regUniformMollifiedInitial ρ ε hε a) ⋯) ⋯ t

The L² path encoded by a coordinate field with the local mild identity is the restriction of the global zero-force mild curve.