OAI/MathematicalPhysics/DefocusingNLS/Certificates/HomotopyCone.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The terminal cone along the tail homotopy

  1. theorem OAI.DefocusingNLS.coneForm_scale line 10
  2. theorem OAI.DefocusingNLS.coneForm_ratio line 24
  3. theorem OAI.DefocusingNLS.coneForm_real_contraction line 29
  4. theorem OAI.DefocusingNLS.coneForm_nonpos_of_contraction line 37
  5. theorem OAI.DefocusingNLS.slowTailRatio_strict_cone line 47
  6. theorem OAI.DefocusingNLS.slowTailRatio_homotopy_cone line 63

    Source documentation

    Every terminal pair in the straight tail homotopy has nonpositive cone.

    theorem slowTailRatio_homotopy_cone (σ : ℝ) (ℓ K : ℕ) (q s : ℂ) (ρ : ℝ)
    (hσ : -(1 / 32 : ℝ) ≤ σ) (hK : 3 ≤ K)
    (hq : q.re = σ + (ℓ : ℝ) / 2) (hsre : s.re = 0) (hsim : s.im ≠ 0)
    (hρ : 0 ≤ ρ) (hρ1 : ρ ≤ 1) :
    coneForm ((ℓ : ℝ) + 5) s ((ρ : ℂ) * slowTailRatio q (ℓ + 6) K s) 1 ≤ 0 :=
…

    Mentions: OAI.DefocusingNLS.coneForm, OAI.DefocusingNLS.slowTailRatio