OAI/Geometry/Convex/GeneralMahler/Density.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The Gaussian integrations in §§02--06: Lebesgue density and translation/scaling dictionary.

  1. abbrev OAI.GeneralMahler.normal line 12
  2. abbrev OAI.GeneralMahler.gamma line 14
  3. def OAI.GeneralMahler.phi line 15
  4. lemma OAI.GeneralMahler.phi_apply line 18
  5. lemma OAI.GeneralMahler.phi_pos line 21
  6. def OAI.GeneralMahler.nDensity line 23
  7. lemma OAI.GeneralMahler.nDensity_pos line 24
  8. lemma OAI.GeneralMahler.continuous_nDensity line 27
  9. lemma OAI.GeneralMahler.nDensity_prod line 30
  10. lemma OAI.GeneralMahler.gaussian_pi_density line 36
  11. theorem OAI.GeneralMahler.normal_density line 61
  12. theorem OAI.GeneralMahler.normal_ac line 80
  13. theorem OAI.GeneralMahler.ac_normal line 83
  14. theorem OAI.GeneralMahler.normal_integral line 91
  15. lemma OAI.GeneralMahler.normal_integrable_iff line 95