OAI/Geometry/Convex/GeneralMahler/Scalar/Integr.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Finite-area bound and infinite tail for K.

  1. def OAI.GeneralMahler.SCal.KP0 line 10
  2. lemma OAI.GeneralMahler.SCal.posKP line 11
  3. lemma OAI.GeneralMahler.SCal.contKP line 12
  4. def OAI.GeneralMahler.SCal.ikp line 13
  5. lemma OAI.GeneralMahler.SCal.idk0 line 14
  6. lemma OAI.GeneralMahler.SCal.ikM line 16
  7. def OAI.GeneralMahler.SCal.zn line 18
  8. lemma OAI.GeneralMahler.SCal.zN0 line 19
  9. lemma OAI.GeneralMahler.SCal.zNm line 20
  10. def OAI.GeneralMahler.SCal.maxArea line 21
  11. def OAI.GeneralMahler.SCal.arSum line 22
  12. lemma OAI.GeneralMahler.SCal.arHI line 25
  13. def OAI.GeneralMahler.SCal.distB line 46
  14. def OAI.GeneralMahler.SCal.AC line 47
  15. lemma OAI.GeneralMahler.SCal.AC_m line 50
  16. lemma OAI.GeneralMahler.SCal.acs line 58
  17. lemma OAI.GeneralMahler.SCal.area0 line 60
  18. def OAI.GeneralMahler.SCal.wI line 74
  19. def OAI.GeneralMahler.SCal.wD line 75
  20. lemma OAI.GeneralMahler.SCal.Eval_log' line 76
  21. lemma OAI.GeneralMahler.SCal.wBound line 80
  22. lemma OAI.GeneralMahler.SCal.w_neg line 92
  23. lemma OAI.GeneralMahler.SCal.wz' line 95
  24. lemma OAI.GeneralMahler.SCal.area_full line 105