HomogeneousRegularCompleteness.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Every C² radial solution belongs to the regular two-column plane.

theorem OAI.DefocusingNLS.valueDet_ne_zero_of_kernel line 14
theorem OAI.DefocusingNLS.homogeneousRegular_basis_complete line 34

theorem OAI.DefocusingNLS.homogeneousRegular_exists_complete_basis line 110

Source documentation

The constructed analytic regular basis is complete for C² radial solutions. The two positions, rather than a prescribed asymptotic expansion, are the only origin regularity data required of the solution.

theorem homogeneousRegular_exists_complete_basis (ell m : ℕ) (νp νm : ℂ)
    (R L : ℝ) (hR : 0 < R) (hL : 0 ≤ L) (Q : ℝ → ℂ) (hQ : Continuous Q) :
    ∃ Vp Vm : ℂ → ℝ → E₄,
      (∀ lam, ‖lam‖ ≤ L → ∀ r ∈ Ioc 0 R, HasDerivAt (Vp lam)
        (spectralPhysicalCircularField (νp - 2 * lam) (νm - 2 * lam)
          ((ell * (ell + 10) : ℕ) : ℂ) m (Q r) r (Vp lam r)) r) ∧
      (∀ lam, ‖lam‖ ≤ L → ∀ r ∈ Ioc 0 R, HasDerivAt (Vm lam)
        (spectralPhysicalCircularField (νp - 2 * lam) (νm - 2 * lam)
          ((ell * (ell + 10) : ℕ) : ℂ) m (Q r) r (Vm lam r)) r) ∧
      (∀ lam, ‖lam‖ ≤ L → LinearIndependent ℂ ![Vp lam R, Vm lam R]) ∧
      (∀ lam, ‖lam‖ ≤ L → ∀ r, 0 ≤ r →
        AnalyticAt ℂ (fun z => Vp z r) lam ∧ AnalyticAt ℂ (fun z => Vm z r) lam) ∧
…

Mentions: OAI.DefocusingNLS.spectralPhysicalCircularField