OAI/Geometry/Convex/GeneralMahler/Frame/Sec.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Divided difference evaluated on two possibly different frames.

  1. def OAI.GeneralMahler.along line 13

    Source comment

    averages on segment
    def along (u:Plane) (t:ℝ) := (1-t)*u.1+t*u.2

    Mentions: OAI.GeneralMahler.Plane

  2. def OAI.GeneralMahler.bav line 14
  3. lemma OAI.GeneralMahler.bav_con line 15
  4. lemma OAI.GeneralMahler.bav_same line 18
  5. lemma OAI.GeneralMahler.delta_eq line 21
  6. lemma OAI.GeneralMahler.bav_bound line 37
  7. def OAI.GeneralMahler.Frm.showM line 59
  8. def OAI.GeneralMahler.Frm.hideM line 60
  9. lemma OAI.GeneralMahler.Frm.reveal line 61
  10. lemma OAI.GeneralMahler.Frm.combine line 64
  11. def OAI.GeneralMahler.Frm.secDiag line 69
  12. def OAI.GeneralMahler.Frm.sec line 71
  13. lemma OAI.GeneralMahler.Frm.sec_eq line 73
  14. lemma OAI.GeneralMahler.Frm.sec_add line 77
  15. lemma OAI.GeneralMahler.Frm.sec_smul line 82
  16. lemma OAI.GeneralMahler.Frm.Aentry line 90
  17. lemma OAI.GeneralMahler.Frm.Bentry line 93
  18. lemma OAI.GeneralMahler.Frm.Aeval line 96
  19. lemma OAI.GeneralMahler.Frm.Beval line 99
  20. lemma OAI.GeneralMahler.Frm.show_sub line 102
  21. lemma OAI.GeneralMahler.Frm.exact_sec line 105
  22. lemma OAI.GeneralMahler.Frm.sec_ind line 117

    Source comment

    Right frame independence for all test kernels on entries
    lemma sec_ind (A B C:Mat m) (g:Plane→ℝ) (hv:v.Dgn B) (hw:w.Dgn B) :
    u.sec v A B g C=u.sec w A B g C := by
…

    Mentions: OAI.GeneralMahler.Mat, OAI.GeneralMahler.Plane