Finite shifts of the global real mild curve

The global mild trajectory restricts continuously to every finite interval after a nonnegative start time.

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

The global real mild curve viewed from a later start time.

Equations

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