OAI/MathematicalPhysics/DefocusingNLS/Certificates/BoundaryMatchingExclusion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exclusion of matching zeros on the left counting boundary

  1. theorem OAI.DefocusingNLS.BoundaryCertificate.boundary_forward_cones_pos line 13
  2. theorem OAI.DefocusingNLS.BoundaryCertificate.boundaryQ_add_nat_ne_zero line 62
  3. theorem OAI.DefocusingNLS.BoundaryCertificate.boundaryQ_sub_mass_add_nat_ne_zero line 73
  4. theorem OAI.DefocusingNLS.BoundaryCertificate.boundaryQ_pochhammer_ne_zero line 86
  5. theorem OAI.DefocusingNLS.BoundaryCertificate.matchingHomotopy_left_boundary_ne_zero line 99

    Source documentation

    No member of the actual tail homotopy has a matching zero on the left counting boundary. The only assumptions are the certified parameter box and the homotopy parameter interval.

    theorem matchingHomotopy_left_boundary_ne_zero (ell : Fin 4) (b Z v ρ : ℝ)
    (hb : |100000000 * b - 33477607| ≤ 2) (hZ : |100000000 * Z - 270506819| ≤ 2)
    (hρ : 0 ≤ ρ) (hρ1 : ρ ≤ 1) :
    matchingColumnDeterminant
      (matchingHomotopyColumn (ell + 5) 8 (Complex.I * Z) ρ (boundaryQ ell b v))
      (matchingHomotopyColumn (ell + 5) 8 (-Complex.I * Z) ρ (boundaryQ ell (-b) v)) ≠ 0 := by
…

    Mentions: OAI.DefocusingNLS.matchingColumnDeterminant, OAI.DefocusingNLS.matchingHomotopyColumn, OAI.DefocusingNLS.BoundaryCertificate.boundaryQ