ExpandingDuhamelRestart.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Restarting the inhomogeneous moving-scale evolution

Splitting the Duhamel integral gives the exact restart identity at the larger radius L exp(s/2). This permits uniform short slabs to be joined.

theorem OAI.DefocusingNLS.expandingDuhamel_eq_intervalIntegral line 17
theorem OAI.DefocusingNLS.expandingFreeStep_after_kernel line 23
theorem OAI.DefocusingNLS.expanding_shifted_kernel line 45

theorem OAI.DefocusingNLS.expandingDuhamel_restart line 60

Source documentation

Exact inhomogeneous restart, with the radius advanced at the restart time.

theorem expandingDuhamel_restart (a b k L s t : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (hs : 0 ≤ s) (ht : 0 ≤ t)
    (r : ℝ → FourierL2) (hr : ContinuousOn r (Icc 0 (s + t))) :
    expandingDuhamel a b k L ha hk hL (s + t) r =
      expandingFreeStep a b k (expandingRadius L s) t ha hk
        (hL.trans (expandingRadius_ge L s hL hs)) ht
        (expandingDuhamel a b k L ha hk hL s r) +
      expandingDuhamel a b k (expandingRadius L s) ha hk
        (hL.trans (expandingRadius_ge L s hL hs)) t (fun u => r (s + u)) := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingDuhamel, OAI.DefocusingNLS.expandingFreeStep, OAI.DefocusingNLS.expandingRadius, OAI.DefocusingNLS.expandingRadius_ge

theorem OAI.DefocusingNLS.expandingMild_restart line 104

Source documentation

Restarting a mild trajectory preserves its actual forcing and advances the radius.

theorem expandingMild_restart (a b k L s t : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (hs : 0 ≤ s) (ht : 0 ≤ t)
    (r : ℝ → FourierL2) (hr : ContinuousOn r (Icc 0 (s + t))) (u₀ : FourierL2) :
    expandingFreeStep a b k L (s + t) ha hk hL (add_nonneg hs ht) u₀ +
      expandingDuhamel a b k L ha hk hL (s + t) r =
    expandingFreeStep a b k (expandingRadius L s) t ha hk
      (hL.trans (expandingRadius_ge L s hL hs)) ht
      (expandingFreeStep a b k L s ha hk hL hs u₀ +
        expandingDuhamel a b k L ha hk hL s r) +
    expandingDuhamel a b k (expandingRadius L s) ha hk
      (hL.trans (expandingRadius_ge L s hL hs)) t (fun u => r (s + u)) := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingFreeStep, OAI.DefocusingNLS.expandingDuhamel, OAI.DefocusingNLS.expandingRadius, OAI.DefocusingNLS.expandingRadius_ge