OAI/MathematicalPhysics/DefocusingNLS/Profile/ProfileCertificateValues.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Exact intermediate rational values for Appendix cert:profile. Every recurrence transition is proved by kernel reduction.

  1. def OAI.DefocusingNLS.ProfileCertificate.Computed.stage0 line 12
  2. def OAI.DefocusingNLS.ProfileCertificate.Computed.stage4 line 14
  3. theorem OAI.DefocusingNLS.ProfileCertificate.Computed.transition4 line 20
  4. def OAI.DefocusingNLS.ProfileCertificate.Computed.stage8 line 23
  5. theorem OAI.DefocusingNLS.ProfileCertificate.Computed.transition8 line 29
  6. def OAI.DefocusingNLS.ProfileCertificate.Computed.stage12 line 32
  7. theorem OAI.DefocusingNLS.ProfileCertificate.Computed.transition12 line 38
  8. def OAI.DefocusingNLS.ProfileCertificate.Computed.stage16 line 41
  9. theorem OAI.DefocusingNLS.ProfileCertificate.Computed.transition16 line 47
  10. def OAI.DefocusingNLS.ProfileCertificate.Computed.stage20 line 50
  11. theorem OAI.DefocusingNLS.ProfileCertificate.Computed.transition20 line 56
  12. def OAI.DefocusingNLS.ProfileCertificate.Computed.stage24 line 59
  13. theorem OAI.DefocusingNLS.ProfileCertificate.Computed.transition24 line 65
  14. def OAI.DefocusingNLS.ProfileCertificate.Computed.stage28 line 68
  15. theorem OAI.DefocusingNLS.ProfileCertificate.Computed.transition28 line 74
  16. def OAI.DefocusingNLS.ProfileCertificate.Computed.stage32 line 77
  17. theorem OAI.DefocusingNLS.ProfileCertificate.Computed.transition32 line 83
  18. def OAI.DefocusingNLS.ProfileCertificate.Computed.stage34 line 86
  19. theorem OAI.DefocusingNLS.ProfileCertificate.Computed.transition34 line 92
  20. theorem OAI.DefocusingNLS.ProfileCertificate.result_eq_computed line 97