OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowUniformAsymptoticBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform leading asymptotic on compact parameter sets

  1. theorem OAI.DefocusingNLS.exists_normalizedSlowSolution_uniform_remainder line 12
  2. theorem OAI.DefocusingNLS.exists_normalizedSlowSolution_compact_remainder line 61

    Source documentation

    Compactness supplies all parameter bounds, including the inverse gamma factor at zero. No exclusion of q=0 is needed.

    theorem exists_normalizedSlowSolution_compact_remainder (m : ℕ) (Q : Set ℂ)
    (hQ : IsCompact Q) (hq : ∀ q ∈ Q, -1 < q.re) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ q ∈ Q, ∀ x : ℂ, 0 ≤ x.re → 1 ≤ ‖x‖ →
      ‖normalizedSlowSolution q m x - 1‖ ≤ C / ‖x‖ := by
…

    Mentions: OAI.DefocusingNLS.normalizedSlowSolution

  3. theorem OAI.DefocusingNLS.exists_compactifiedSlowSolution_compact_bound line 84