OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialAngularUpperExclusion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Upper real-part exclusion in every spherical-harmonic channel of the actual profile.

  1. def OAI.DefocusingNLS.HasAngularSpectralSystem line 18

    Source documentation

    The four real equations with angular eigenvalue η = ℓ(ℓ+10).

    def HasAngularSpectralSystem (n : ℕ) (z : ProfileMatchingBall) (η σ τ : ℝ)
    (f : Fin 4 → ℝ → ℝ) : Prop := ∀ r, 0 ≤ r →
…
  2. theorem OAI.DefocusingNLS.radialMatched_angular_upper_exclusion line 29