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

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Algebraic reduction of equation (4).

  1. def OAI.GeneralMahler.SCal.SE.pPlus line 12
  2. def OAI.GeneralMahler.SCal.SE.qPlus line 13
  3. def OAI.GeneralMahler.SCal.SE.pa line 14
  4. def OAI.GeneralMahler.SCal.SE.pd line 15
  5. def OAI.GeneralMahler.SCal.SE.ba line 16
  6. def OAI.GeneralMahler.SCal.SE.bd0 line 17
  7. def OAI.GeneralMahler.SCal.SE.ca0 line 18
  8. def OAI.GeneralMahler.SCal.SE.cd0 line 19
  9. def OAI.GeneralMahler.SCal.SE.ek line 20
  10. def OAI.GeneralMahler.SCal.SE.costs line 21
  11. lemma OAI.GeneralMahler.SCal.SE.vdis_swap line 24
  12. lemma OAI.GeneralMahler.SCal.SE.rsum_eq line 26
  13. lemma OAI.GeneralMahler.SCal.SE.dsum_eq line 27
  14. lemma OAI.GeneralMahler.SCal.SE.gamma_swap line 29
  15. lemma OAI.GeneralMahler.SCal.SE.lid4 line 31
  16. def OAI.GeneralMahler.SCal.SE.refPt line 44

    Source comment

    Reflection combined with swapping
    def refPt (x:Plane):Plane :=(-x.2,-x.1)

    Mentions: OAI.GeneralMahler.Plane

  17. lemma OAI.GeneralMahler.SCal.SE.bavRefE line 46
  18. lemma OAI.GeneralMahler.SCal.SE.bavRefO line 52
  19. lemma OAI.GeneralMahler.SCal.SE.mRefE line 58
  20. lemma OAI.GeneralMahler.SCal.SE.mRefO line 67
  21. lemma OAI.GeneralMahler.SCal.SE.cost_ref line 76
  22. lemma OAI.GeneralMahler.SCal.SE.neg_left line 94