OAI/Geometry/Convex/GeneralMahler/CovHerm.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Eq13 coefficient-pair (weighted K multiplier via coefficients).

  1. def OAI.GeneralMahler.Pj line 12
  2. def OAI.GeneralMahler.Pt line 13
  3. def OAI.GeneralMahler.PJ line 15
  4. lemma OAI.GeneralMahler.pJ_eq line 20
  5. def OAI.GeneralMahler.CpPair line 22
  6. def OAI.GeneralMahler.kMode line 23
  7. def OAI.GeneralMahler.KP line 24
  8. lemma OAI.GeneralMahler.pt_sum line 26
  9. lemma OAI.GeneralMahler.summable_k line 32
  10. lemma OAI.GeneralMahler.K_sum line 43
  11. lemma OAI.GeneralMahler.ProjField.regH line 48
  12. lemma OAI.GeneralMahler.ProjField.cfH_sym line 50
  13. lemma OAI.GeneralMahler.ProjField.pj_sum line 54
  14. lemma OAI.GeneralMahler.ProjField.pt_k_cov line 72