OAI/Geometry/Convex/GeneralMahler/Hermite/L2.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Scalar coefficient calculus.

  1. abbrev OAI.GeneralMahler.HMode.G2 line 10
  2. def OAI.GeneralMahler.HMode.ModL line 11
  3. lemma OAI.GeneralMahler.HMode.ModL_ae line 14
  4. def OAI.GeneralMahler.HMode.qcf line 15
  5. lemma OAI.GeneralMahler.HMode.qcf_ip line 18
  6. lemma OAI.GeneralMahler.HMode.qcf_ip' line 24
  7. lemma OAI.GeneralMahler.HMode.qcf_congr line 27
  8. lemma OAI.GeneralMahler.HMode.Mod_o line 33
  9. def OAI.GeneralMahler.HMode.HB line 40
  10. lemma OAI.GeneralMahler.HMode.HB_eq line 51
  11. lemma OAI.GeneralMahler.HMode.repr_eq line 53
  12. lemma OAI.GeneralMahler.HMode.qcf_sum line 56