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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Completion of short widths (≤.16), with explicit rounded budgets.

  1. lemma OAI.GeneralMahler.SCal.SE.endDa line 12
  2. lemma OAI.GeneralMahler.SCal.SE.CDa line 29
  3. lemma OAI.GeneralMahler.SCal.SE.smallF line 53
  4. lemma OAI.GeneralMahler.SCal.SE.cost_small line 63
  5. lemma OAI.GeneralMahler.SCal.SE.reduce_f line 107
  6. lemma OAI.GeneralMahler.SCal.SE.short line 115