OAI/MathematicalPhysics/DefocusingNLS/Certificates/HorizontalForwardLink.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.horizontalQ line 11
2. theorem OAI.DefocusingNLS.horizontalDifference_forward line 14
3. theorem OAI.DefocusingNLS.horizontalState_forward line 34
4. theorem OAI.DefocusingNLS.normalizedForwardJet_cone_sum line 67

   Source documentation

   The finite telescoping identity retains the exact cone weights.

   theorem normalizedForwardJet_cone_sum (ell N : ℕ) (h σ b Z v : ℝ)
       (hv : v ≠ 0) (hd : ∀ n : ℕ, horizontalQ ell h σ b v + n - (ell + 5) ≠ 0)
       (B C : ℂ) :
       coneForm ((ell : ℝ) + 5) ((h : ℂ) * Complex.I * Z)
         (normalizedForwardJet (ell + 5) ((h : ℂ) * Complex.I * Z)
           (horizontalQ ell h σ b v) ![B, (v : ℂ) * C] N 0)
         (normalizedForwardJet (ell + 5) ((h : ℂ) * Complex.I * Z)
           (horizontalQ ell h σ b v) ![B, (v : ℂ) * C] N 1) =
       coneForm ((ell : ℝ) + 5) ((h : ℂ) * Complex.I * Z) B ((v : ℂ) * C) +
         horizontalIncrementSum ell h σ b Z v⁻¹ B C N := by
   …

   Mentions: OAI.DefocusingNLS.horizontalQ, OAI.DefocusingNLS.coneForm, OAI.DefocusingNLS.normalizedForwardJet, OAI.DefocusingNLS.horizontalIncrementSum