OAI/MathematicalPhysics/DefocusingNLS/Certificates/CentralZeroTailCount.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The numerical central zero-tail count in a counting rectangle

  1. theorem OAI.DefocusingNLS.SeparatorArithmetic.central_zeroTail_zero_of_polynomial_root line 13
  2. theorem OAI.DefocusingNLS.SeparatorArithmetic.exists_central_zeroTail_rectangle_count line 23

    Source documentation

    Every sufficiently tall counting rectangle contains exactly the certified number of zero-tail zeros, counted by their analytic orders.

    theorem exists_central_zeroTail_rectangle_count (ell : Fin 4) :
    ∃ V : ℝ, 0 < V ∧ ∀ W : ℝ, V < W →
      rectangleZeroCount W
        (spectralHomotopyDeterminant ell (33477607 / 100000000) (270506819 / 100000000) 0) =
          (positiveRootCount ell : ℕ∞) := by
…

    Mentions: OAI.DefocusingNLS.rectangleZeroCount, OAI.DefocusingNLS.spectralHomotopyDeterminant, OAI.DefocusingNLS.SeparatorArithmetic.positiveRootCount