OAI/Geometry/Convex/GeneralMahler/Budget/Eq19.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Budgets on remainder by Hermite degree.

  1. lemma OAI.GeneralMahler.sigEQ line 12
  2. lemma OAI.GeneralMahler.odd_budget line 20
  3. def OAI.GeneralMahler.bmp line 34
  4. lemma OAI.GeneralMahler.bmp_pos line 35
  5. lemma OAI.GeneralMahler.bm_pos line 36
  6. lemma OAI.GeneralMahler.even_budget line 39
  7. lemma OAI.GeneralMahler.ProjField.cov_bound line 68
  8. lemma OAI.GeneralMahler.ProjField.sig_one_degree line 72
  9. lemma OAI.GeneralMahler.ProjField.degree19 line 137
  10. lemma OAI.GeneralMahler.ProjField.NTpos19 line 157