OAI/MathematicalPhysics/DefocusingNLS/Certificates/HorizontalCompactification.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.horizontalDifference line 11
2. def OAI.DefocusingNLS.horizontalState line 17
3. theorem OAI.DefocusingNLS.horizontalDifference_zero line 24
4. theorem OAI.DefocusingNLS.horizontalState_zero line 32
5. def OAI.DefocusingNLS.horizontalIncrementSum line 43
6. theorem OAI.DefocusingNLS.horizontalIncrementSum_zero line 50
7. theorem OAI.DefocusingNLS.horizontal_limiting_form_pos line 67

   Source documentation

   The horizontal limiting form is uniformly positive in the counting strip. No asymptotic assumption is used: this is the exact value at inverse frequency zero.

   theorem horizontal_limiting_form_pos (ell : ℕ) (σ b Z : ℝ) (B C : ℂ)
       (hσ : -(1 / 32 : ℝ) ≤ σ) (hZ : Z ≠ 0) (hBC : B ≠ 0 ∨ C ≠ 0) :
       0 < ((ell : ℝ) + 5) * Complex.normSq B +
         horizontalIncrementSum ell 1 σ b Z 0 B C 8 +
         horizontalIncrementSum ell (-1) σ b Z 0 B C 8 := by
   …

   Mentions: OAI.DefocusingNLS.horizontalIncrementSum