OAI/Geometry/Convex/GeneralMahler/Angle.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Inward normalization estimate: layer as seen in a unit direction.

  1. def OAI.GeneralMahler.ProjField.dimH line 14
  2. lemma OAI.GeneralMahler.ProjField.h_between line 17
  3. def OAI.GeneralMahler.ProjField.vp line 30
  4. lemma OAI.GeneralMahler.ProjField.S_vp line 32
  5. lemma OAI.GeneralMahler.ProjField.dimH_X line 35
  6. lemma OAI.GeneralMahler.ProjField.dimH_Y line 41
  7. lemma OAI.GeneralMahler.ProjField.form_da line 70
  8. lemma OAI.GeneralMahler.ProjField.whole line 85
  9. lemma OAI.GeneralMahler.ProjField.diff_int line 93
  10. lemma OAI.GeneralMahler.ProjField.int_pst line 97
  11. lemma OAI.GeneralMahler.ProjField.p_step_zero line 100
  12. lemma OAI.GeneralMahler.ProjField.step_int line 109
  13. def OAI.GeneralMahler.ProjField.plus line 113
  14. def OAI.GeneralMahler.ProjField.minus line 114
  15. lemma OAI.GeneralMahler.ProjField.pn line 116
  16. lemma OAI.GeneralMahler.ProjField.plus_int line 130
  17. lemma OAI.GeneralMahler.ProjField.minus_int line 133