OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffMildResidual.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The exact mild defect has the proved small cutoff-residual bound

  1. theorem OAI.DefocusingNLS.expandingDuhamel_complex_smul line 15
  2. def OAI.DefocusingNLS.sampledCutoffNonlinearHistory line 26
  3. theorem OAI.DefocusingNLS.continuous_sampledCutoffNonlinearHistory line 34
  4. theorem OAI.DefocusingNLS.sampledCutoffProfile_mild_residual line 44
  5. theorem OAI.DefocusingNLS.exists_cutoffProfile_mild_residual_bound line 85

    Source documentation

    The true mild defect is uniformly small in the initial torus scale.

    theorem exists_cutoffProfile_mild_residual_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 : β„•) (ham : 2 * a * (m : ℝ) = 1) :
    βˆƒ N : β„•, βˆ€ (Q : E β†’ β„‚) (hQ : ContDiff ℝ ∞ Q) (D : ℝ), 0 ≀ D β†’
      (βˆ€ n ≀ N, βˆ€ y : E, y β‰  0 β†’
        β€–iteratedFDeriv ℝ n Q yβ€– ≀ D * β€–yβ€– ^ (-2 * a - (n : ℝ))) β†’
      (βˆ€ y, stationarySimilarityDefect a b m Q y = 0) β†’
      βˆƒ C : ℝ, 0 ≀ C ∧ βˆ€ (L T : ℝ) (hL : 1 ≀ L) (hT : 0 ≀ T) (t : ℝ)
        (ht : t ∈ Icc 0 T),
…

    Mentions: OAI.DefocusingNLS.stationarySimilarityDefect