OAI/MathematicalPhysics/DefocusingNLS/Certificates/HorizontalMatchingExclusion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.horizontalQ_im line 15
2. theorem OAI.DefocusingNLS.horizontalQ_re line 18
3. theorem OAI.DefocusingNLS.horizontalQ_im_ne_zero line 21
4. theorem OAI.DefocusingNLS.horizontalQ_sub_mass_add_ne_zero line 29
5. theorem OAI.DefocusingNLS.horizontal_homotopyColumn_ne_zero line 37
6. theorem OAI.DefocusingNLS.horizontal_homotopy_cone_nonpos line 48
7. theorem OAI.DefocusingNLS.horizontal_forward_forms_pos line 72
8. theorem OAI.DefocusingNLS.matchingHomotopy_horizontal_ne_zero_of_form line 107

   Source documentation

   The finite positive form excludes horizontal homotopy zeros. Its uniform positivity is supplied by exists_horizontal_positive_neighborhood.

   theorem matchingHomotopy_horizontal_ne_zero_of_form (ell : ℕ) (σ b Z v ρ : ℝ)
       (hσ : -(1 / 32 : ℝ) ≤ σ) (hZ : Z ≠ 0) (hbv : |b| < |v|)
       (hρ : 0 ≤ ρ) (hρ1 : ρ ≤ 1)
       (hform : ∀ B C : ℂ, B ≠ 0 ∨ C ≠ 0 →
         0 < horizontalFormAt ell (v⁻¹, σ, b, Z, B, C)) :
       matchingColumnDeterminant
         (matchingHomotopyColumn (ell + 5) 8 ((1 : ℂ) * Complex.I * Z) ρ
           (horizontalQ ell 1 σ b v))
         (matchingHomotopyColumn (ell + 5) 8 ((-1 : ℂ) * Complex.I * Z) ρ
           (horizontalQ ell (-1) σ b v)) ≠ 0 := by
   …

   Mentions: OAI.DefocusingNLS.horizontalFormAt, OAI.DefocusingNLS.matchingColumnDeterminant, OAI.DefocusingNLS.matchingHomotopyColumn, OAI.DefocusingNLS.horizontalQ