OAI/Geometry/Convex/GeneralMahler/Middle/Prefix.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Vertex checking via prefix integrals.

  1. def OAI.GeneralMahler.SCal.Mid.ptF line 9
  2. def OAI.GeneralMahler.SCal.Mid.pz line 16
  3. lemma OAI.GeneralMahler.SCal.Mid.pv line 17
  4. def OAI.GeneralMahler.SCal.Mid.aStep line 29
  5. abbrev OAI.GeneralMahler.SCal.Mid.PrefixC line 30
  6. def OAI.GeneralMahler.SCal.Mid.Works line 31
  7. lemma OAI.GeneralMahler.SCal.Mid.stays line 33
  8. def OAI.GeneralMahler.SCal.Mid.signF line 40
  9. def OAI.GeneralMahler.SCal.Mid.fo line 41
  10. def OAI.GeneralMahler.SCal.Mid.sFt line 42
  11. def OAI.GeneralMahler.SCal.Mid.sP line 43
  12. lemma OAI.GeneralMahler.SCal.Mid.fFlip line 45
  13. lemma OAI.GeneralMahler.SCal.Mid.integralFneg line 55
  14. lemma OAI.GeneralMahler.SCal.Mid.sumNeg line 65
  15. def OAI.GeneralMahler.SCal.Mid.EB line 82
  16. def OAI.GeneralMahler.SCal.Mid.mj line 83
  17. lemma OAI.GeneralMahler.SCal.Mid.mj_ok line 86
  18. def OAI.GeneralMahler.SCal.Mid.ins line 109
  19. def OAI.GeneralMahler.SCal.Mid.dotE line 111
  20. lemma OAI.GeneralMahler.SCal.Mid.dot_ok line 112