OAI/MathematicalPhysics/DefocusingNLS/Profile/ProfileCertificateRecipe.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The exact K=34 recipe of the manuscript, Appendix cert:profile. All operations here are rational. Its analytic interpretation is established separately; no certificate comparison is assumed.

  1. abbrev OAI.DefocusingNLS.ProfileCertificate.QMatrix line 11
  2. abbrev OAI.DefocusingNLS.ProfileCertificate.RMatrix line 12
  3. def OAI.DefocusingNLS.ProfileCertificate.centerB line 14
  4. def OAI.DefocusingNLS.ProfileCertificate.centerZ line 15
  5. def OAI.DefocusingNLS.ProfileCertificate.radius line 16
  6. def OAI.DefocusingNLS.ProfileCertificate.parameterB line 18
  7. def OAI.DefocusingNLS.ProfileCertificate.parameterZ line 19
  8. def OAI.DefocusingNLS.ProfileCertificate.majorant line 20
  9. def OAI.DefocusingNLS.ProfileCertificate.factor line 24
  10. structure OAI.DefocusingNLS.ProfileCertificate.State line 28
  11. def OAI.DefocusingNLS.ProfileCertificate.initial line 35
  12. def OAI.DefocusingNLS.ProfileCertificate.step line 38

    Source documentation

    All four right-hand sides use the old state, as in the supplement.

    def step (n : ℕ) (s : State) : State :=
…

    Mentions: OAI.DefocusingNLS.ProfileCertificate.State

  13. def OAI.DefocusingNLS.ProfileCertificate.result line 54

    Source documentation

    Descending multiplication of factors 33 through 0.

    def result : State := (List.range 34).foldr step initial

    Mentions: OAI.DefocusingNLS.ProfileCertificate.State, OAI.DefocusingNLS.ProfileCertificate.step, OAI.DefocusingNLS.ProfileCertificate.initial

  14. def OAI.DefocusingNLS.ProfileCertificate.normalized line 56
  15. def OAI.DefocusingNLS.ProfileCertificate.changeBound line 59
  16. def OAI.DefocusingNLS.ProfileCertificate.denominatorGap line 61
  17. def OAI.DefocusingNLS.ProfileCertificate.jetError line 66
  18. def OAI.DefocusingNLS.ProfileCertificate.tailError line 69