Uniform complete Sobolev candidate from a later time

At every nonnegative start time, the global mild curve supplies a bounded physical coefficient for a complete Sobolev mild equation on the same uniform time step.

theorem CKN.Leray.regularisedBesselShiftedLinearCandidate (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) (b₀ : ↥RealVectorL2) (hbJ : RegularizedMildJData b₀) (a : ℝ) (ha : 0 ≤ a) : let T := regularisedBesselUniformEnergyStep ρ ε hε k ‖b₀‖; let g := regularisedGlobalComplexShiftPath ρ ε hε b₀ hbJ a T; ∃ (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)), regularisedBesselLinearLocalMap ρ ε hε k b T ⋯ g ‖b₀‖ ⋯ ⋯ v = v ∧ ‖v‖ ≤ 2 * ‖b‖

From any nonnegative start time and complete Sobolev initial state, the equation linearized around the shifted global mild curve has an H²ᵏ solution on a time step fixed by the initial physical L² bound.