OAI/Analysis/Steinitz/GaussianKernel.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Diagonal Gaussian kernels and their densities.

  1. def OAI.GaussianKernel.diagonalLaw line 15
  2. instance OAI.GaussianKernel.(instance at line 18) line 18
  3. def OAI.GaussianKernel.density line 23
  4. lemma OAI.GaussianKernel.density_nonneg line 26
  5. lemma OAI.GaussianKernel.density_continuous line 29
  6. lemma OAI.GaussianKernel.pi_density line 33
  7. lemma OAI.GaussianKernel.diagonalLaw_density line 49
  8. lemma OAI.GaussianKernel.density_pos line 66
  9. lemma OAI.GaussianKernel.density_neg line 70
  10. lemma OAI.GaussianKernel.density_le_zero line 76
  11. lemma OAI.GaussianKernel.charFun_diagonalLaw line 88
  12. def OAI.GaussianKernel.scaleMap line 101
  13. lemma OAI.GaussianKernel.scaleMap_apply line 104
  14. lemma OAI.GaussianKernel.stdGaussian_map_scale line 109
  15. lemma OAI.GaussianKernel.density_exp line 137
  16. lemma OAI.GaussianKernel.density_integrable line 154
  17. lemma OAI.GaussianKernel.stdGaussian_eq_density line 160
  18. lemma OAI.GaussianKernel.linear_image_density line 165