OAI/Probability/GaussianPropeller/GaussianCoordinates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GaussianPropeller.Analytic.covariance_inner_stdGaussian line 35
2. lemma OAI.GaussianPropeller.Analytic.hasGaussianLaw_innerFamily line 40
3. lemma OAI.GaussianPropeller.Analytic.indep_innerFamily line 45
4. lemma OAI.GaussianPropeller.Analytic.map_inner_stdGaussian line 50
5. lemma OAI.GaussianPropeller.Analytic.map_orthonormal_stdGaussian line 56
6. lemma OAI.GaussianPropeller.Analytic.map_orthonormal_triple_stdGaussian line 78
7. lemma OAI.GaussianPropeller.Analytic.lintegral_orthonormal_triple line 90