OAI/Probability/ProjectionMoments/GaussianDensity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ProjectionMoments.stdGaussian_le_volume line 15
2. lemma OAI.ProjectionMoments.stdGaussian_submodule_null line 29
3. lemma OAI.ProjectionMoments.gaussian_rows_ae_gramSchmidt_ne_zero line 34
4. lemma OAI.ProjectionMoments.gaussian_rows_ae_linearIndependent line 66
5. lemma OAI.ProjectionMoments.lintegral_gaussianReal_sq line 73
6. lemma OAI.ProjectionMoments.lintegral_stdGaussian_norm_sq line 83
7. lemma OAI.ProjectionMoments.gaussian_norm_ball_mass line 102
8. lemma OAI.ProjectionMoments.map_withDensity_equiv line 134
9. lemma OAI.ProjectionMoments.density_moment_equiv line 148