OAI/MathematicalPhysics/DefocusingNLS/Certificates/SeparatorScaling.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Scaling between the integer certificate and the zero-tail polynomial

  1. theorem OAI.DefocusingNLS.SeparatorArithmetic.scaled_monomial line 13
  2. theorem OAI.DefocusingNLS.SeparatorArithmetic.scaledSeparatorPolynomial_identity line 21
  3. theorem OAI.DefocusingNLS.SeparatorArithmetic.scaledSeparatorPolynomial_roots line 36
  4. theorem OAI.DefocusingNLS.SeparatorArithmetic.closed_half_plane_count_image_pos line 46
  5. theorem OAI.DefocusingNLS.SeparatorArithmetic.windingPolynomial_closed_half_plane_count line 62

    Source documentation

    Exact half-plane count for the unscaled polynomial appearing in the manuscript's zero-tail winding argument.

    theorem windingPolynomial_closed_half_plane_count (ℓ : Fin 4) :
    ((((windingPolynomial ℓ).map (Int.castRingHom ℂ)).roots.toFinset).filter
      (fun z => 0 ≤ z.re)).card = positiveRootCount ℓ := by
…

    Mentions: OAI.DefocusingNLS.SeparatorArithmetic.windingPolynomial, OAI.DefocusingNLS.SeparatorArithmetic.positiveRootCount