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

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Vanishing of all chaos coefficients implies vanishing a.e.; proof via an exponential integrability and characteristic function argument.

  1. lemma OAI.GeneralMahler.HMode.lp_poly line 11
  2. lemma OAI.GeneralMahler.HMode.lp_EXP line 16
  3. lemma OAI.GeneralMahler.HMode.momentPower line 37
  4. lemma OAI.GeneralMahler.HMode.wave_zero line 74
  5. lemma OAI.GeneralMahler.HMode.pospart_char line 116
  6. lemma OAI.GeneralMahler.HMode.measurable_zero line 132
  7. theorem OAI.GeneralMahler.HMode.ae_zero line 179