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

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Hermite modes and Gaussian averages via TestF. Probabilists' convention, orthonormal scaling.

  1. def OAI.GeneralMahler.ga line 11
  2. lemma OAI.GeneralMahler.ga_i line 12
  3. lemma OAI.GeneralMahler.ga_add line 14
  4. lemma OAI.GeneralMahler.ga_sub line 17
  5. lemma OAI.GeneralMahler.ga_mul line 20
  6. lemma OAI.GeneralMahler.ga_parts line 24
  7. lemma OAI.GeneralMahler.ga_pair line 36
  8. lemma OAI.GeneralMahler.gamma_area line 48
  9. def OAI.GeneralMahler.HMode.sn line 54
  10. lemma OAI.GeneralMahler.HMode.snsq line 55
  11. lemma OAI.GeneralMahler.HMode.sn_succ line 56
  12. def OAI.GeneralMahler.HMode.H line 58
  13. lemma OAI.GeneralMahler.HMode.ht line 61
  14. lemma OAI.GeneralMahler.HMode.raise line 65
  15. lemma OAI.GeneralMahler.HMode.lower line 67
  16. lemma OAI.GeneralMahler.HMode.Hder line 91
  17. lemma OAI.GeneralMahler.HMode.avg_succ line 96
  18. lemma OAI.GeneralMahler.HMode.avg_z line 102
  19. lemma OAI.GeneralMahler.HMode.avg_o line 104