OAI/Geometry/Convex/GeneralMahler/Linear/Eq26.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

§06 weighted Dirichlet inequality.

  1. def OAI.GeneralMahler.ProjField.locJ line 13
  2. lemma OAI.GeneralMahler.ProjField.DLherm line 15
  3. lemma OAI.GeneralMahler.ProjField.DJi line 17
  4. lemma OAI.GeneralMahler.ProjField.locJ_form line 21
  5. lemma OAI.GeneralMahler.ProjField.mDout line 29
  6. lemma OAI.GeneralMahler.ProjField.Rpt_eq line 38
  7. lemma OAI.GeneralMahler.ProjField.Jpt_eq line 47
  8. lemma OAI.GeneralMahler.ProjField.R_nu line 56
  9. lemma OAI.GeneralMahler.ProjField.J_nu line 64
  10. lemma OAI.GeneralMahler.ProjField.J_sum line 71
  11. lemma OAI.GeneralMahler.ProjField.J_vec line 77
  12. lemma OAI.GeneralMahler.ProjField.S_W line 85
  13. lemma OAI.GeneralMahler.ProjField.S_pair line 90
  14. lemma OAI.GeneralMahler.ProjField.eq26pt line 93
  15. lemma OAI.GeneralMahler.ProjField.eq26sum line 103
  16. lemma OAI.GeneralMahler.ProjField.eq26 line 120