OAI/Geometry/Convex/GeneralMahler/ProfileGrowth.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Profile regularity by derivative recurrences and log tail bounds.

  1. lemma OAI.GeneralMahler.Profile.Y_limitbound line 11
  2. lemma OAI.GeneralMahler.Profile.f_poly line 16
  3. lemma OAI.GeneralMahler.Profile.f_bounds line 19
  4. lemma OAI.GeneralMahler.Profile.X2f_poly line 31
  5. lemma OAI.GeneralMahler.Profile.Y2j_poly line 58
  6. lemma OAI.GeneralMahler.Profile.X_M line 61
  7. lemma OAI.GeneralMahler.Profile.Y_M line 64
  8. lemma OAI.GeneralMahler.Profile.g_poly line 68
  9. lemma OAI.GeneralMahler.Profile.gd_poly line 72
  10. lemma OAI.GeneralMahler.Profile.d_poly line 77
  11. lemma OAI.GeneralMahler.Profile.v_test line 83
  12. lemma OAI.GeneralMahler.Profile.moderate_dg line 84
  13. lemma OAI.GeneralMahler.Profile.g_test line 100
  14. lemma OAI.GeneralMahler.Profile.d_test line 101