OAI/MathematicalPhysics/DefocusingNLS/Certificates/RationalComplexMatrix.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Exact complex rational arithmetic for the finite profile certificate.

  1. abbrev OAI.DefocusingNLS.ProfileCertificate.RationalComplex line 12
  2. def OAI.DefocusingNLS.ProfileCertificate.RationalComplex.normSq line 16
  3. def OAI.DefocusingNLS.ProfileCertificate.RationalComplex.absOne line 18
  4. def OAI.DefocusingNLS.ProfileCertificate.RationalComplex.quotient line 20
  5. def OAI.DefocusingNLS.ProfileCertificate.RationalComplex.toComplex line 24
  6. theorem OAI.DefocusingNLS.ProfileCertificate.RationalComplex.toComplex_re line 31
  7. theorem OAI.DefocusingNLS.ProfileCertificate.RationalComplex.toComplex_im line 32
  8. theorem OAI.DefocusingNLS.ProfileCertificate.RationalComplex.normSq_toComplex line 34
  9. theorem OAI.DefocusingNLS.ProfileCertificate.RationalComplex.norm_toComplex_le_absOne line 38
  10. theorem OAI.DefocusingNLS.ProfileCertificate.RationalComplex.toComplex_quotient line 43
  11. structure OAI.DefocusingNLS.ProfileCertificate.Matrix2 line 50

    Source documentation

    A computational four-entry matrix, avoiding dependent finite-index evaluation.

    @[ext] structure Matrix2 (R : Type*) where
…
  12. def OAI.DefocusingNLS.ProfileCertificate.Matrix2.zero line 61
  13. def OAI.DefocusingNLS.ProfileCertificate.Matrix2.one line 62
  14. def OAI.DefocusingNLS.ProfileCertificate.Matrix2.add line 63
  15. def OAI.DefocusingNLS.ProfileCertificate.Matrix2.mul line 65
  16. def OAI.DefocusingNLS.ProfileCertificate.Matrix2.scale line 68
  17. def OAI.DefocusingNLS.ProfileCertificate.Matrix2.map line 70
  18. def OAI.DefocusingNLS.ProfileCertificate.Matrix2.toMatrix line 72
  19. theorem OAI.DefocusingNLS.ProfileCertificate.Matrix2.toMatrix_zero line 75
  20. theorem OAI.DefocusingNLS.ProfileCertificate.Matrix2.toMatrix_one line 77
  21. theorem OAI.DefocusingNLS.ProfileCertificate.Matrix2.toMatrix_add line 79
  22. theorem OAI.DefocusingNLS.ProfileCertificate.Matrix2.toMatrix_mul line 82
  23. theorem OAI.DefocusingNLS.ProfileCertificate.Matrix2.toMatrix_scale line 86
  24. theorem OAI.DefocusingNLS.ProfileCertificate.Matrix2.toMatrix_map line 89