OAI/Geometry/Convex/GeneralMahler/Scalar/Tail/Limit.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

§07 log domain elementary envelope values.

  1. def OAI.GeneralMahler.SCal.Tail.y0 line 10
  2. lemma OAI.GeneralMahler.SCal.Tail.ey0 line 11
  3. lemma OAI.GeneralMahler.SCal.Tail.ro_lim line 12
  4. lemma OAI.GeneralMahler.SCal.Tail.vsmall line 24
  5. lemma OAI.GeneralMahler.SCal.Tail.econ line 34
  6. lemma OAI.GeneralMahler.SCal.Tail.Q_limit line 63
  7. def OAI.GeneralMahler.SCal.Tail.xiMax line 97

    Source comment

    base envelope Boxes
    def xiMax:IV:=(1:IV)/IV.c 4096
  8. def OAI.GeneralMahler.SCal.Tail.XI line 98
  9. def OAI.GeneralMahler.SCal.Tail.BI line 99
  10. def OAI.GeneralMahler.SCal.Tail.wb line 100
  11. def OAI.GeneralMahler.SCal.Tail.wr line 101
  12. def OAI.GeneralMahler.SCal.Tail.pf0 line 104
  13. def OAI.GeneralMahler.SCal.Tail.pr line 105
  14. def OAI.GeneralMahler.SCal.Tail.m0B line 109
  15. def OAI.GeneralMahler.SCal.Tail.mr line 113
  16. lemma OAI.GeneralMahler.SCal.Tail.lXI line 119
  17. lemma OAI.GeneralMahler.SCal.Tail.lBI line 121
  18. lemma OAI.GeneralMahler.SCal.Tail.lwb line 122
  19. lemma OAI.GeneralMahler.SCal.Tail.lwr line 128
  20. lemma OAI.GeneralMahler.SCal.Tail.lpF line 132
  21. lemma OAI.GeneralMahler.SCal.Tail.lTm0 line 143
  22. lemma OAI.GeneralMahler.SCal.Tail.lTm line 160