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

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Chord kernel bounds sharp enough for all midpoints.

  1. lemma OAI.GeneralMahler.SCal.SE.sh0 line 12
  2. def OAI.GeneralMahler.SCal.SE.pm line 14
  3. lemma OAI.GeneralMahler.SCal.SE.θpm line 15
  4. lemma OAI.GeneralMahler.SCal.SE.negpm line 19
  5. lemma OAI.GeneralMahler.SCal.SE.pm_square line 25
  6. lemma OAI.GeneralMahler.SCal.SE.Wmax line 55
  7. lemma OAI.GeneralMahler.SCal.SE.sh_line line 64
  8. lemma OAI.GeneralMahler.SCal.SE.cfac line 72
  9. lemma OAI.GeneralMahler.SCal.SE.sfac line 73
  10. lemma OAI.GeneralMahler.SCal.SE.pm_vsq line 77
  11. lemma OAI.GeneralMahler.SCal.SE.Wpar line 113