OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialUpperExclusion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Upper real-part exclusion in the radial channel of the actual matched profile.

  1. def OAI.DefocusingNLS.HasRadialSpectralSystem line 17

    Source documentation

    The four real equations for a radial complexified spectral mode.

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