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

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Tower AD for exp, log, inverse, square root.

  1. def OAI.GeneralMahler.Jet.vn line 9
  2. def OAI.GeneralMahler.Jet.invJs line 10
  3. def OAI.GeneralMahler.Jet.rootJs line 13
  4. def OAI.GeneralMahler.Jet.logJs line 16
  5. def OAI.GeneralMahler.Jet.expSub line 21

    Source comment

    utilities (exp evaluation an external input)
    def expSub {α} [Add α] [Mul α] (X:J α) (a:α) : J α :=
…

    Mentions: OAI.GeneralMahler.Jet.J

  6. def OAI.GeneralMahler.Jet.invSub line 23
  7. def OAI.GeneralMahler.Jet.logSub line 25
  8. def OAI.GeneralMahler.Jet.rootSub line 27
  9. lemma OAI.GeneralMahler.Jet.twInvs line 30
  10. lemma OAI.GeneralMahler.Jet.twRoots line 45
  11. lemma OAI.GeneralMahler.Jet.twLogs line 61
  12. lemma OAI.GeneralMahler.Jet.TW.inv line 66
  13. lemma OAI.GeneralMahler.Jet.TW.root line 67
  14. lemma OAI.GeneralMahler.Jet.TW.log line 69
  15. lemma OAI.GeneralMahler.Jet.TW.exp line 71
  16. def OAI.GeneralMahler.Jet.ub line 77
  17. lemma OAI.GeneralMahler.Jet.ubb line 78
  18. lemma OAI.GeneralMahler.Jet.fitsInv line 81
  19. lemma OAI.GeneralMahler.Jet.Fits.inv line 85
  20. lemma OAI.GeneralMahler.Jet.Fits.rt line 87
  21. lemma OAI.GeneralMahler.Jet.Fits.log line 93
  22. lemma OAI.GeneralMahler.Jet.Fits.exp line 99