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

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Circular means on normalized interval and variance inequality.

  1. def OAI.GeneralMahler.SCal.SE.cott line 11
  2. def OAI.GeneralMahler.SCal.SE.PhiA line 13
  3. def OAI.GeneralMahler.SCal.SE.PhiB line 14
  4. def OAI.GeneralMahler.SCal.SE.fstar line 15
  5. def OAI.GeneralMahler.SCal.SE.Pastar line 16
  6. def OAI.GeneralMahler.SCal.SE.Pdstar line 17
  7. abbrev OAI.GeneralMahler.SCal.SE.Fxc line 19
  8. abbrev OAI.GeneralMahler.SCal.SE.Fxs line 20
  9. lemma OAI.GeneralMahler.SCal.SE.dcx line 21
  10. lemma OAI.GeneralMahler.SCal.SE.dsx line 23
  11. lemma OAI.GeneralMahler.SCal.SE.phaseAC line 25
  12. lemma OAI.GeneralMahler.SCal.SE.lc_rot line 82
  13. lemma OAI.GeneralMahler.SCal.SE.ls_rot line 84
  14. lemma OAI.GeneralMahler.SCal.SE.bcirc line 86
  15. lemma OAI.GeneralMahler.SCal.SE.PSum line 104
  16. lemma OAI.GeneralMahler.SCal.SE.init_phase line 110