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

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Exterior square-root kernel integrals in §05.

  1. def OAI.GeneralMahler.Roots.u line 10
  2. def OAI.GeneralMahler.Roots.p line 11
  3. def OAI.GeneralMahler.Roots.xk line 12
  4. def OAI.GeneralMahler.Roots.yk line 13
  5. lemma OAI.GeneralMahler.Roots.u_pos line 14
  6. lemma OAI.GeneralMahler.Roots.u_add line 15
  7. lemma OAI.GeneralMahler.Roots.sqrt_top line 18
  8. lemma OAI.GeneralMahler.Roots.sqrt_bot line 23
  9. lemma OAI.GeneralMahler.Roots.t_p line 26
  10. lemma OAI.GeneralMahler.Roots.p_lt line 33
  11. lemma OAI.GeneralMahler.Roots.dp line 39
  12. lemma OAI.GeneralMahler.Roots.x_formula line 58
  13. lemma OAI.GeneralMahler.Roots.y_formula line 65
  14. lemma OAI.GeneralMahler.Roots.pu_limit line 77
  15. lemma OAI.GeneralMahler.Roots.cu line 92
  16. def OAI.GeneralMahler.Roots.fx line 94
  17. def OAI.GeneralMahler.Roots.fy line 95
  18. lemma OAI.GeneralMahler.Roots.dfx line 96
  19. lemma OAI.GeneralMahler.Roots.dfy line 107
  20. lemma OAI.GeneralMahler.Roots.area_template line 113
  21. lemma OAI.GeneralMahler.Roots.puc line 120
  22. lemma OAI.GeneralMahler.Roots.x_area line 122
  23. lemma OAI.GeneralMahler.Roots.y_area line 135