OAI/MathematicalPhysics/DefocusingNLS/Certificates/FreeLowAngularSpectrum.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The low angular outgoing counts on the manuscript's parameter disk

  1. def OAI.DefocusingNLS.freeMatchingDisk line 13

    Source documentation

    The exact disk in equation free:parameter-disk; terminating decimals are represented as rational numbers.

    def freeMatchingDisk : Set (ℝ × ℝ) :=
…
  2. theorem OAI.DefocusingNLS.freeMatchingDisk_subset_certificate_box line 17
  3. def OAI.DefocusingNLS.closedCountingHalfPlaneZeroCount line 34
  4. theorem OAI.DefocusingNLS.spectralSlowDeterminant_left_ne_zero line 37
  5. theorem OAI.DefocusingNLS.closedCountingHalfPlaneZeroCount_eq_open line 44
  6. theorem OAI.DefocusingNLS.free_low_angular_count line 64

    Source documentation

    The low modes of Proposition free:main, on its exact disk and closed counting half-plane.

    theorem free_low_angular_count (hR : RectangleRouche) (ell : Fin 4) (b Z : ℝ)
    (h : (b, Z) ∈ freeMatchingDisk) :
    closedCountingHalfPlaneZeroCount (spectralSlowDeterminant ell b Z) =
      (SeparatorArithmetic.positiveRootCount ell : ℕ∞) := by
…

    Mentions: OAI.DefocusingNLS.RectangleRouche, OAI.DefocusingNLS.freeMatchingDisk, OAI.DefocusingNLS.closedCountingHalfPlaneZeroCount, OAI.DefocusingNLS.spectralSlowDeterminant, OAI.DefocusingNLS.SeparatorArithmetic.positiveRootCount