Complex mild equation after a global restart #
Every nonnegative shift of the global real mild curve satisfies the corresponding translated complex L² Volterra equation.
theorem
CKN.Leray.regularisedGlobalComplexShiftPath_linearMild
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(b₀ : ↥RealVectorL2)
(hbJ : RegularizedMildJData b₀)
(a T : ℝ)
(ha : 0 ≤ a)
(hT : 0 ≤ T)
(t : ↑(RegularizedMildTimeInterval T))
:
have g := regularisedGlobalComplexShiftPath ρ ε hε b₀ hbJ a T;
g t = heatSemigroup ↑t ⋯ (complexifyVectorL2 (regularizedGlobalMildCurve ρ ε hε b₀ hbJ a)) - ∫ (τ : ℝ) in 0..T, if h : 0 < τ ∧ τ < ↑t then
stokesL2Operator ⋯
(((regularisedTensorPhysicalMap ρ ε hε) (g (regularizedMildTimeClamp T hT (↑t - τ))))
(g (regularizedMildTimeClamp T hT (↑t - τ))))
else 0
The shifted global mild curve solves the complex linear equation with its own L² path as prescribed tensor coefficient.