OAI/MathematicalPhysics/DefocusingNLS/Certificates/HorizontalContinuity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DefocusingNLS.HorizontalParameters line 13

   Source documentation

   Real spectral part, shift, coupling, and the two normalized initial coordinates.

   abbrev HorizontalParameters := ℝ × ℝ × ℝ × ℂ × ℂ

2. def OAI.DefocusingNLS.horizontalStateAt line 15
3. def OAI.DefocusingNLS.horizontalDifferenceAt line 19
4. theorem OAI.DefocusingNLS.continuousAt_horizontalStateAt line 24
5. theorem OAI.DefocusingNLS.continuousAt_horizontalDifferenceAt line 44
6. def OAI.DefocusingNLS.horizontalFormAt line 53
7. theorem OAI.DefocusingNLS.continuousAt_horizontalFormAt line 58
8. theorem OAI.DefocusingNLS.eventually_horizontalForm_positive line 75

   Source documentation

   Compactness makes the positive limiting form uniform over all normalized initial data and spectral parameters in a compact set.

   theorem eventually_horizontalForm_positive (ell : ℕ) (P : Set HorizontalParameters)
       (hP : IsCompact P) (hσ : ∀ p ∈ P, -(1 / 32 : ℝ) ≤ p.1)
       (hZ : ∀ p ∈ P, p.2.2.1 ≠ 0)
       (hBC : ∀ p ∈ P, p.2.2.2.1 ≠ 0 ∨ p.2.2.2.2 ≠ 0) :
       ∀ᶠ τ in 𝓝 (0 : ℝ), ∀ p ∈ P, 0 < horizontalFormAt ell (τ, p) := by
   …

   Mentions: OAI.DefocusingNLS.HorizontalParameters, OAI.DefocusingNLS.horizontalFormAt