OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffResidualDuhamel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.sampledCutoffResidualHistory line 15
2. theorem OAI.DefocusingNLS.continuous_sampledCutoffResidualHistory line 24
3. theorem OAI.DefocusingNLS.exists_cutoffResidual_Duhamel_bound line 37

   Source documentation

   The free response to the actual residual retains the small scale factor, with a constant independent of the starting radius and the length of the slab.

   theorem exists_cutoffResidual_Duhamel_bound (a b k : ℝ)
       (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k)
       (χ : 𝓢(E, ℝ)) (hχ : HasCompactSupport (χ : E → ℝ))
       (hχone : ∀ x : E, ‖x‖ < 1 / 2 → χ x = 1)
       (hχzero : ∀ x : E, 2 < ‖x‖ → χ x = 0) (m : ℕ) :
       ∃ N : ℕ, ∀ (Q : E → ℂ) (hQ : ContDiff ℝ ∞ Q) (D : ℝ), 0 ≤ D →
         (∀ n ≤ N, ∀ y : E, y ≠ 0 →
           ‖iteratedFDeriv ℝ n Q y‖ ≤ D * ‖y‖ ^ (-2 * a - (n : ℝ))) →
         ∃ C : ℝ, 0 ≤ C ∧ ∀ (L T : ℝ) (hL : 1 ≤ L) (hT : 0 ≤ T) (t : ℝ),
           t ∈ Icc 0 T →
           ‖expandingDuhamel a b k L ha hk hL t
             (sampledCutoffResidualHistory a k L T ha ha1 hk hL hT
   …

   Mentions: OAI.DefocusingNLS.expandingDuhamel, OAI.DefocusingNLS.sampledCutoffResidualHistory