OAI/MathematicalPhysics/DefocusingNLS/Certificates/CenteredPolynomial.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Denominator-cleared Taylor coefficients for the disk certificates

  1. def OAI.DefocusingNLS.SeparatorArithmetic.windingPolynomial line 16

    Source documentation

    The full unscaled winding polynomial, with integer coefficients.

    def windingPolynomial (ℓ : ℕ) : Polynomial ℤ :=
…
  2. theorem OAI.DefocusingNLS.SeparatorArithmetic.coeff_windingPolynomial line 19
  3. theorem OAI.DefocusingNLS.SeparatorArithmetic.windingPolynomial_matches_product line 29

    Source documentation

    The coefficient description holds at every order, including the vanishing tail, so this polynomial is exactly the coefficientwise imaginary product.

    theorem windingPolynomial_matches_product (ℓ j : ℕ) :
    (windingPolynomial ℓ).coeff j =
      ((toPolynomial (backwardCoefficients ℓ).1 *
        (toPolynomial (backwardCoefficients ℓ).2).map
          (starRingEnd GaussianInt)).coeff j).im := by
…

    Mentions: OAI.DefocusingNLS.SeparatorArithmetic.windingPolynomial, OAI.DefocusingNLS.SeparatorArithmetic.toPolynomial, OAI.DefocusingNLS.SeparatorArithmetic.backwardCoefficients

  4. theorem OAI.DefocusingNLS.SeparatorArithmetic.coeff_taylor_finite line 36
  5. def OAI.DefocusingNLS.SeparatorArithmetic.scaledSeparatorPolynomial line 58

    Source documentation

    Polynomial before translation, with the scaling denominator cleared.

    def scaledSeparatorPolynomial (ℓ : ℕ) : Polynomial GaussianInt :=
…
  6. theorem OAI.DefocusingNLS.SeparatorArithmetic.centeredCoefficient_eq line 62