OAI/MathematicalPhysics/DefocusingNLS/Profile/NormalizedSlowCone.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.normalizedSlow_tail_nontrivial line 11
2. theorem OAI.DefocusingNLS.normalizedSlow_cone_increment line 40
3. theorem OAI.DefocusingNLS.normalizedSlow_strict_cone line 54
4. theorem OAI.DefocusingNLS.normalizedSlow_tail_disk line 90

   Source documentation

   The tail denominator is nonzero and its ratio lies in the strict disk, including at q = 0.

   theorem normalizedSlow_tail_disk (σ : ℝ) (ℓ K : ℕ) (q s : ℂ)
       (hσ : -(1 / 32 : ℝ) ≤ σ) (hK : 3 ≤ K)
       (hq : q.re = σ + (ℓ : ℝ) / 2) (hsre : s.re = 0) (hsim : s.im ≠ 0) :
       normalizedSlowC q (ℓ + 6) s K ≠ 0 ∧
         Complex.normSq (normalizedSlowB q (ℓ + 6) s K / normalizedSlowC q (ℓ + 6) s K +
           s / ((ℓ : ℝ) + 5 : ℂ)) < Complex.normSq (s / ((ℓ : ℝ) + 5 : ℂ)) := by
   …

   Mentions: OAI.DefocusingNLS.normalizedSlowC, OAI.DefocusingNLS.normalizedSlowB