OAI/Geometry/Convex/GeneralMahler/Beta.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

§04 Eq15, threshold comparison.

  1. lemma OAI.GeneralMahler.pj_cont line 12
  2. lemma OAI.GeneralMahler.pj_p line 18
  3. lemma OAI.GeneralMahler.pj_M line 27
  4. def OAI.GeneralMahler.ProjField.betaK line 38
  5. def OAI.GeneralMahler.ProjField.be line 39
  6. def OAI.GeneralMahler.ProjField.nTK line 40
  7. def OAI.GeneralMahler.ProjField.Nt line 41
  8. lemma OAI.GeneralMahler.ProjField.bMS line 43
  9. lemma OAI.GeneralMahler.ProjField.nMS line 51
  10. def OAI.GeneralMahler.ProjField.RadiusE line 65
  11. lemma OAI.GeneralMahler.ProjField.ER_P line 66
  12. lemma OAI.GeneralMahler.ProjField.ER_hi line 67
  13. lemma OAI.GeneralMahler.ProjField.beyond line 70
  14. def OAI.GeneralMahler.ProjField.crossK line 80
  15. lemma OAI.GeneralMahler.ProjField.crossMS line 82
  16. lemma OAI.GeneralMahler.ProjField.point_expand_f line 105
  17. lemma OAI.GeneralMahler.ProjField.point_expand line 131
  18. lemma OAI.GeneralMahler.ProjField.square_pt line 140
  19. lemma OAI.GeneralMahler.ProjField.eq15 line 174