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

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Piecewise kernel square estimates will use these scaled integrable majorants.

  1. def OAI.GeneralMahler.Roots.slab line 11
  2. def OAI.GeneralMahler.Roots.U line 13
  3. lemma OAI.GeneralMahler.Roots.slab_int line 16
  4. lemma OAI.GeneralMahler.Roots.secU line 42
  5. lemma OAI.GeneralMahler.Roots.U_area line 57
  6. def OAI.GeneralMahler.Roots.gx line 65
  7. lemma OAI.GeneralMahler.Roots.g_area line 66
  8. def OAI.GeneralMahler.Roots.Ux line 77
  9. def OAI.GeneralMahler.Roots.Uy line 78
  10. lemma OAI.GeneralMahler.Roots.Ux_area line 79
  11. lemma OAI.GeneralMahler.Roots.Uy_area line 83
  12. lemma OAI.GeneralMahler.Roots.U_swap line 88
  13. lemma OAI.GeneralMahler.Roots.U_outHi line 89
  14. lemma OAI.GeneralMahler.Roots.U_outLo line 95
  15. lemma OAI.GeneralMahler.Roots.U_mid line 100