OAI/Geometry/Convex/GeneralMahler/Linear/Segments.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

End point profile tests for Eq26-27. Segment condition Eq4 (proved in scalar part).

  1. lemma OAI.GeneralMahler.Segment.Wav line 12
  2. lemma OAI.GeneralMahler.Segment.bav_sym line 13
  3. lemma OAI.GeneralMahler.Segment.bav_add line 25
  4. lemma OAI.GeneralMahler.Segment.bav_scale line 30
  5. lemma OAI.GeneralMahler.Segment.bav_const line 32
  6. lemma OAI.GeneralMahler.Segment.Wflip line 33
  7. lemma OAI.GeneralMahler.Segment.Wsq line 35
  8. def OAI.GeneralMahler.Segment.rest line 38

    Source documentation

    remainder of scalar profile. bstar uses A profile.

    def rest (f:ℝ→ℝ) (u:Plane) := bav f u-f u.1

    Mentions: OAI.GeneralMahler.Plane, OAI.GeneralMahler.bav

  9. def OAI.GeneralMahler.Segment.dis line 39
  10. def OAI.GeneralMahler.Segment.sqav line 40
  11. def OAI.GeneralMahler.Segment.mdis line 41
  12. def OAI.GeneralMahler.Segment.vdis line 42
  13. def OAI.GeneralMahler.Segment.vsum line 43
  14. def OAI.GeneralMahler.Segment.rsum line 44
  15. def OAI.GeneralMahler.Segment.dsum line 45
  16. def OAI.GeneralMahler.Segment.bstar line 46
  17. def OAI.GeneralMahler.Segment.anti line 47
  18. def OAI.GeneralMahler.Segment.sgamma line 48
  19. def OAI.GeneralMahler.Segment.resid line 50
  20. def OAI.GeneralMahler.Segment.symR line 52
  21. def OAI.GeneralMahler.Segment.SegmentOK line 53
  22. lemma OAI.GeneralMahler.Segment.mdis_eq line 56
  23. lemma OAI.GeneralMahler.Segment.Wr line 65
  24. lemma OAI.GeneralMahler.Segment.Ws line 66
  25. lemma OAI.GeneralMahler.Segment.Wm line 67
  26. lemma OAI.GeneralMahler.Segment.Wv line 70
  27. lemma OAI.GeneralMahler.Segment.Wa line 72
  28. lemma OAI.GeneralMahler.Segment.Wg line 73
  29. lemma OAI.GeneralMahler.Segment.Wd line 77
  30. lemma OAI.GeneralMahler.Segment.Wb line 79
  31. lemma OAI.GeneralMahler.Segment.Wvs line 81
  32. lemma OAI.GeneralMahler.Segment.Wres line 83
  33. lemma OAI.GeneralMahler.Segment.WR line 86
  34. lemma OAI.GeneralMahler.Segment.diagR line 89
  35. lemma OAI.GeneralMahler.Segment.Rflip line 96
  36. lemma OAI.GeneralMahler.Segment.negR line 97
  37. lemma OAI.GeneralMahler.Segment.Rle line 102