OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffPicardResidual.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The sampled cutoff is a quantitative approximate Picard fixed point

  1. theorem OAI.DefocusingNLS.cutoffNonlinearHistory_eq_reaction line 15
  2. theorem OAI.DefocusingNLS.exists_cutoffPicard_residual_bound line 25

    Source documentation

    The approximate fixed-point error has no dependence on the slab length.

    theorem exists_cutoffPicard_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),
        let q := sampledCutoffProfilePath a k L T ha ha1 hk hL
…

    Mentions: OAI.DefocusingNLS.stationarySimilarityDefect, OAI.DefocusingNLS.sampledCutoffProfilePath

  3. theorem OAI.DefocusingNLS.exists_cutoffProfile_shortSlab_stability line 74

    Source documentation

    On a short slab, every bounded exact trajectory close to the sampled stationary cutoff remains close with the actual L^(-2-a) forcing error.

    theorem exists_cutoffProfile_shortSlab_stability (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) (R : ℝ) (hR : 0 ≀ R) :
    βˆƒ K : ℝ, 0 ≀ K ∧ βˆƒ 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 * K < 1 β†’
        let q := sampledCutoffProfilePath a k L T ha ha1 hk hL
…

    Mentions: OAI.DefocusingNLS.stationarySimilarityDefect, OAI.DefocusingNLS.sampledCutoffProfilePath