OAI/Geometry/Convex/GeneralMahler/Segment/First.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Combine chord and endpoint variation using pointwise U star.

  1. def OAI.GeneralMahler.SCal.SE.alongD line 11
  2. def OAI.GeneralMahler.SCal.SE.alongN line 12
  3. lemma OAI.GeneralMahler.SCal.SE.hoD line 13
  4. def OAI.GeneralMahler.SCal.SE.GammaB line 26
  5. lemma OAI.GeneralMahler.SCal.SE.gmBound line 27
  6. def OAI.GeneralMahler.SCal.SE.negN line 52
  7. lemma OAI.GeneralMahler.SCal.SE.ekB line 53
  8. lemma OAI.GeneralMahler.SCal.SE.smallU line 64
  9. lemma OAI.GeneralMahler.SCal.SE.chAbs line 93