Time shifts of the global complex mild curve

Every nonnegative start time gives a continuous bounded complex L² coefficient path for the uniform complete Sobolev continuation equation.

noncomputable def CKN.Leray.regularisedGlobalComplexShiftPath (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b₀ : ↥RealVectorL2) (hbJ : RegularizedMildJData b₀) (a T : ℝ) : C(↑(RegularizedMildTimeInterval T), ↥ComplexVectorL2)

The complex global mild curve shifted to a nonnegative start time.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.regularisedGlobalComplexShiftPath_norm_le_initial (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b₀ : ↥RealVectorL2) (hbJ : RegularizedMildJData b₀) (a T : ℝ) (ha : 0 ≤ a) (q : ↑(RegularizedMildTimeInterval T)) : ‖(regularisedGlobalComplexShiftPath ρ ε hε b₀ hbJ a T) q‖ ≤ ‖b₀‖

Every nonnegative shift has the same global physical L² bound.