OAI/MathematicalPhysics/DefocusingNLS/Certificates/HorizontalUniformPositivity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.horizontalParameterBox line 11
2. theorem OAI.DefocusingNLS.isCompact_horizontalParameterBox line 14
3. theorem OAI.DefocusingNLS.horizontalParameterBox_nonzero line 18
4. theorem OAI.DefocusingNLS.exists_horizontal_positive_neighborhood line 30

   Source documentation

   One inverse-frequency neighborhood works for the full parameter box and all unit initial vectors. The estimate is symmetric in positive/negative frequency.

   theorem exists_horizontal_positive_neighborhood (ell : ℕ) (R b₀ b₁ Z₀ Z₁ : ℝ)
       (hZ : 0 < Z₀) :
       ∃ ε : ℝ, 0 < ε ∧ ∀ τ : ℝ, |τ| < ε →
         ∀ p ∈ horizontalParameterBox R b₀ b₁ Z₀ Z₁, 0 < horizontalFormAt ell (τ, p) := by
   …

   Mentions: OAI.DefocusingNLS.horizontalParameterBox, OAI.DefocusingNLS.horizontalFormAt