CutoffResidualSampling.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The exact cutoff residual has expanding-torus norm O(L^(-2-a))

def OAI.DefocusingNLS.cutoffResidualSchwartz line 14
theorem OAI.DefocusingNLS.cutoffResidualSchwartz_apply line 22
theorem OAI.DefocusingNLS.exists_cutoffResidual_sampling_bound line 39

theorem OAI.DefocusingNLS.exists_actualCutoffResidual_bound line 82

Source documentation

The sampled object in the norm estimate represents exactly the three displayed terms of the physical PDE residual.

theorem exists_actualCutoffResidual_bound (a k : ℝ) (ha : 0 < a)
    (ha1 : a < 1) (hk : 8 < k) (m : ℕ) (ham : 2 * a * (m : ℝ) = 1)
    (χ : 𝓢(E, ℝ)) (hχ : HasCompactSupport (χ : E → ℝ))
    (hχone : ∀ x : E, ‖x‖ < 1 / 2 → χ x = 1)
    (hχzero : ∀ x : E, 2 < ‖x‖ → χ x = 0) :
    ∃ 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 : ℝ) (hL : 1 ≤ L), ∃ R : 𝓢(E, ℂ),
        (∀ y : E, R y = cutoffResidual m L χ Q y) ∧
        ‖schwartzTorusSample a k L ha1 hk hL (radianFourierKernel R)‖ ≤
          C * L ^ (-2 - a) := by
…

Mentions: OAI.DefocusingNLS.cutoffResidual, OAI.DefocusingNLS.schwartzTorusSample, OAI.DefocusingNLS.radianFourierKernel