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

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Tensor Hermite modes, Gaussian multivariate.

  1. abbrev OAI.GeneralMahler.HMode.MI line 12
  2. abbrev OAI.GeneralMahler.HMode.e line 13
  3. def OAI.GeneralMahler.HMode.MM line 14
  4. def OAI.GeneralMahler.HMode.inc line 15
  5. def OAI.GeneralMahler.HMode.decM line 16
  6. lemma OAI.GeneralMahler.HMode.inc_at line 17
  7. lemma OAI.GeneralMahler.HMode.dec_at line 18
  8. lemma OAI.GeneralMahler.HMode.p_finprod line 20
  9. lemma OAI.GeneralMahler.HMode.M_poly line 26
  10. lemma OAI.GeneralMahler.HMode.M_diff line 28
  11. lemma OAI.GeneralMahler.HMode.M_cont line 38
  12. lemma OAI.GeneralMahler.HMode.M_inner line 40
  13. lemma OAI.GeneralMahler.HMode.factor line 60
  14. lemma OAI.GeneralMahler.HMode.factor_upd line 64
  15. lemma OAI.GeneralMahler.HMode.ee line 72
  16. lemma OAI.GeneralMahler.HMode.ladder line 74
  17. lemma OAI.GeneralMahler.HMode.dir_line line 79
  18. lemma OAI.GeneralMahler.HMode.part_lower line 83