HomogeneousDuhamelRestart.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact whole-space restart and real linearity of the Duhamel operator

theorem OAI.DefocusingNLS.continuous_homogeneousKernel line 13

theorem OAI.DefocusingNLS.homogeneousDuhamel_restart line 21

Source documentation

Splitting the integral gives restart at every real pair of times.

theorem homogeneousDuhamel_restart (a b k s t : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k)
    (r : ℝ → HomogeneousY a k) (hr : Continuous r) :
    homogeneousDuhamel a b k ha ha1 hk (s + t) r =
      homogeneousFreeOperator a b k t ha ha1 hk (homogeneousDuhamel a b k ha ha1 hk s r) +
        homogeneousDuhamel a b k ha ha1 hk t (fun u => r (s + u)) := by
…

Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousDuhamel, OAI.DefocusingNLS.homogeneousFreeOperator

theorem OAI.DefocusingNLS.homogeneousDuhamel_zero line 54
theorem OAI.DefocusingNLS.homogeneousDuhamel_add line 59
theorem OAI.DefocusingNLS.homogeneousDuhamel_real_smul line 69