OAI/MathematicalPhysics/DefocusingNLS/Certificates/ZeroTailConjugation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Conjugation of the two zero-tail matching channels

  1. theorem OAI.DefocusingNLS.SeparatorArithmetic.backwardProduct_conjugate line 14
  2. theorem OAI.DefocusingNLS.SeparatorArithmetic.zeroTailQ_conjugate line 27
  3. theorem OAI.DefocusingNLS.SeparatorArithmetic.zeroTailS_conjugate line 33
  4. theorem OAI.DefocusingNLS.SeparatorArithmetic.evaluate_conjugate_polynomial line 36
  5. theorem OAI.DefocusingNLS.SeparatorArithmetic.evaluatePair_conjugate line 41
  6. theorem OAI.DefocusingNLS.SeparatorArithmetic.windingPolynomial_complex_identity line 59

    Source documentation

    The imaginary-part coefficients encode the full determinant polynomial, not merely its values on the real axis.

    theorem windingPolynomial_complex_identity (ell : ℕ) :
    C (2 * Complex.I) * (windingPolynomial ell).map (Int.castRingHom ℂ) =
      (toPolynomial (backwardCoefficients ell).1 *
        (toPolynomial (backwardCoefficients ell).2).map (starRingEnd GaussianInt)).map
          GaussianInt.toComplex -
      ((toPolynomial (backwardCoefficients ell).1 *
        (toPolynomial (backwardCoefficients ell).2).map (starRingEnd GaussianInt)).map
          GaussianInt.toComplex).map (starRingEnd ℂ) := by
…

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