Local mild solution for regularized Leray evolution

The contraction on the lifespan of eq:reg-lifespan gives the solution of lem:reg-local-mild, including its initial value and uniqueness among all continuous spatial L² mild trajectories.

theorem CKN.Leray.regularizedMildLocalSolution (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (hb : RegularizedMildJData b) : ∃ (u : C(↑(RegularizedMildTimeInterval (regularizedMildLocalLifespan ρ ε b)), ↥RealVectorL2)), IsRegularizedMildTrajectory ρ ε hε b (regularizedMildLocalLifespan ρ ε b) u ∧ (∀ (t : ↑(RegularizedMildTimeInterval (regularizedMildLocalLifespan ρ ε b))), RegularizedMildJData (u t)) ∧ u ⟨0, ⋯⟩ = b ∧ ∀ (v : C(↑(RegularizedMildTimeInterval (regularizedMildLocalLifespan ρ ε b)), ↥RealVectorL2)), IsRegularizedMildTrajectory ρ ε hε b (regularizedMildLocalLifespan ρ ε b) v → v = u

Local existence and unrestricted mild uniqueness in lem:reg-local-mild. The trajectory takes values in the divergence-free closed subspace.