OAI/Geometry/Convex/GeneralMahler/Middle/Features.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Center profiles for direct evaluation in compact region.

  1. inductive OAI.GeneralMahler.SCal.Mid.Ft line 9
  2. instance OAI.GeneralMahler.SCal.Mid.(instance at line 13) line 13
  3. def OAI.GeneralMahler.SCal.Mid.k0 line 18
  4. def OAI.GeneralMahler.SCal.Mid.c0 line 19
  5. def OAI.GeneralMahler.SCal.Mid.q0 line 20
  6. def OAI.GeneralMahler.SCal.Mid.Ft.f line 22
  7. def OAI.GeneralMahler.SCal.Mid.Ft.g line 29
  8. def OAI.GeneralMahler.SCal.Mid.Ft.cK line 30
  9. def OAI.GeneralMahler.SCal.Mid.Ft.cC line 31
  10. def OAI.GeneralMahler.SCal.Mid.Ft.cP line 32
  11. def OAI.GeneralMahler.SCal.Mid.Ft.cJ line 33
  12. def OAI.GeneralMahler.SCal.Mid.Ft.cap line 34
  13. lemma OAI.GeneralMahler.SCal.Mid.Ft.test line 40
  14. lemma OAI.GeneralMahler.SCal.Mid.Ft.shiftGuard line 50
  15. lemma OAI.GeneralMahler.SCal.Mid.Ft.guardQ line 65
  16. lemma OAI.GeneralMahler.SCal.Mid.Ft.guardCS line 72
  17. lemma OAI.GeneralMahler.SCal.Mid.Ft.guarded line 108