OAI/MathematicalPhysics/DefocusingNLS/Certificates/OutgoingHalfPlaneCount.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Numerical outgoing counts in the full counting half-plane

  1. def OAI.DefocusingNLS.countingHalfPlaneZeroCount line 11
  2. theorem OAI.DefocusingNLS.countingHalfPlaneZeroCount_eq_rectangle line 14
  3. theorem OAI.DefocusingNLS.spectralSlowDeterminant_ne_zero_of_endpoint line 30
  4. theorem OAI.DefocusingNLS.exists_countingHalfPlaneZeroCount_eq_rectangle line 37
  5. theorem OAI.DefocusingNLS.central_outgoing_halfPlane_count line 61

    Source documentation

    The central outgoing determinant has zero count 2, 1, 0, 0 in the half-plane Re(z)>-1/32, conditional only on Ahlfors's Rouché corollary.

    theorem central_outgoing_halfPlane_count (hR : RectangleRouche) (ell : Fin 4) :
    countingHalfPlaneZeroCount
      (spectralSlowDeterminant ell (33477607 / 100000000) (270506819 / 100000000)) =
        (SeparatorArithmetic.positiveRootCount ell : ℕ∞) := by
…

    Mentions: OAI.DefocusingNLS.RectangleRouche, OAI.DefocusingNLS.countingHalfPlaneZeroCount, OAI.DefocusingNLS.spectralSlowDeterminant, OAI.DefocusingNLS.SeparatorArithmetic.positiveRootCount