OAI/MathematicalPhysics/DefocusingNLS/Certificates/CentralOutgoingCount.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Conditional numerical outgoing counts at the certified central parameters

  1. theorem OAI.DefocusingNLS.exists_central_outgoing_rectangle_count line 12

    Source documentation

    The actual outgoing determinant has the certified count, with multiplicity, in every sufficiently tall rectangle. Only the published rectangle Rouché proposition is assumed.

    theorem exists_central_outgoing_rectangle_count (hR : RectangleRouche) (ell : Fin 4) :
    ∃ V : ℝ, 0 < V ∧ ∀ W : ℝ, V < W →
      rectangleZeroCount W
        (spectralSlowDeterminant ell (33477607 / 100000000) (270506819 / 100000000)) =
          (SeparatorArithmetic.positiveRootCount ell : ℕ∞) := by
…

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