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

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A posteriori approximation of functional via actual f bounded derivatives.

  1. lemma OAI.GeneralMahler.SCal.Mid.cap_le line 10
  2. lemma OAI.GeneralMahler.SCal.Mid.Ast_in line 12
  3. def OAI.GeneralMahler.SCal.Mid.stepG line 16
  4. lemma OAI.GeneralMahler.SCal.Mid.ndS line 17
  5. lemma OAI.GeneralMahler.SCal.Mid.ratio01 line 20
  6. lemma OAI.GeneralMahler.SCal.Mid.len_cmp line 35
  7. def OAI.GeneralMahler.SCal.Mid.perE line 46
  8. lemma OAI.GeneralMahler.SCal.Mid.chordFeat line 47
  9. def OAI.GeneralMahler.SCal.Mid.rectA line 83
  10. def OAI.GeneralMahler.SCal.Mid.areaP line 84
  11. lemma OAI.GeneralMahler.SCal.Mid.area_pair line 85
  12. lemma OAI.GeneralMahler.SCal.Mid.arealine line 91
  13. def OAI.GeneralMahler.SCal.Mid.accum line 121
  14. lemma OAI.GeneralMahler.SCal.Mid.sum_pair line 124