OAI/Geometry/Convex/GeneralMahler/Intervals/Elem.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Interval square root and exponential.

  1. def OAI.GeneralMahler.Cert.IV.piB line 6
  2. lemma OAI.GeneralMahler.Cert.IV.mpi line 8
  3. def OAI.GeneralMahler.Cert.IV.isrt line 14
  4. def OAI.GeneralMahler.Cert.IV.getR line 17
  5. def OAI.GeneralMahler.Cert.IV.rlo line 22
  6. def OAI.GeneralMahler.Cert.IV.rtB line 24
  7. lemma OAI.GeneralMahler.Cert.IV.callSq line 32
  8. lemma OAI.GeneralMahler.Cert.IV.Lsq line 34
  9. lemma OAI.GeneralMahler.Cert.IV.Usq line 41
  10. lemma OAI.GeneralMahler.Cert.IV.mrt line 49
  11. def OAI.GeneralMahler.Cert.IV.eSeries line 68
  12. lemma OAI.GeneralMahler.Cert.IV.mSeries line 74
  13. def OAI.GeneralMahler.Cert.IV.terr line 90

    Source comment

    error < 1e-24 through terms n=0:24.
    def terr : IV := box (-1000000) 1000000

    Mentions: OAI.GeneralMahler.Cert.IV

  14. def OAI.GeneralMahler.Cert.IV.esmall line 92
  15. lemma OAI.GeneralMahler.Cert.IV.mesmall line 94
  16. def OAI.GeneralMahler.Cert.IV.ebox line 110
  17. lemma OAI.GeneralMahler.Cert.IV.mebox line 116