OAI/MathematicalPhysics/DefocusingNLS/Certificates/BoundaryCertificateArithmetic.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The integer boundary certificate recipe

The depth-eight forward recurrence gives coefficient enclosures for the boundary determinant and its homogeneous chart transforms.

  1. abbrev OAI.DefocusingNLS.BoundaryCertificate.EnclosurePolynomial line 14
  2. def OAI.DefocusingNLS.BoundaryCertificate.coefficient line 16
  3. def OAI.DefocusingNLS.BoundaryCertificate.constant line 17
  4. def OAI.DefocusingNLS.BoundaryCertificate.sharpAux line 19
  5. def OAI.DefocusingNLS.BoundaryCertificate.sharp line 24
  6. abbrev OAI.DefocusingNLS.BoundaryCertificate.Row line 26
  7. abbrev OAI.DefocusingNLS.BoundaryCertificate.State line 27
  8. def OAI.DefocusingNLS.BoundaryCertificate.step line 29
  9. def OAI.DefocusingNLS.BoundaryCertificate.state line 40
  10. def OAI.DefocusingNLS.BoundaryCertificate.hermitian line 44
  11. def OAI.DefocusingNLS.BoundaryCertificate.symmetrize line 50
  12. def OAI.DefocusingNLS.BoundaryCertificate.determinant line 52
  13. def OAI.DefocusingNLS.BoundaryCertificate.evenCoefficients line 60

    Source documentation

    The degree-30 real-even truncation. Its use requires the structural proof.

    def evenCoefficients (ell : ℕ) : List GaussianEnclosure :=
…

    Mentions: OAI.DefocusingNLS.GaussianEnclosure

  14. def OAI.DefocusingNLS.BoundaryCertificate.transformAux line 65
  15. def OAI.DefocusingNLS.BoundaryCertificate.transformed line 74
  16. def OAI.DefocusingNLS.BoundaryCertificate.coefficientPositive line 77
  17. def OAI.DefocusingNLS.BoundaryCertificate.positiveFirst16 line 80