OAI/Probability/LogConcave/Analysis/GaussianCoefficient.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LogConcaveSampling.map_withDensity_of_measurePreserving line 16
2. def OAI.LogConcaveSampling.EulerDensity.gaussianCoefficient line 33
3. lemma OAI.LogConcaveSampling.EulerDensity.standard_pi_density line 36
4. theorem OAI.LogConcaveSampling.EulerDensity.standard_density line 57
5. lemma OAI.LogConcaveSampling.EulerDensity.gaussianCoefficient_positive line 77
6. lemma OAI.LogConcaveSampling.EulerDensity.gaussianCoefficient_finite line 83
7. lemma OAI.LogConcaveSampling.EulerDensity.standard_partition line 86
8. def OAI.LogConcaveSampling.EulerDensity.shear line 97
9. lemma OAI.LogConcaveSampling.EulerDensity.shear_measurePreserving line 106
10. lemma OAI.LogConcaveSampling.EulerDensity.map_withDensity_equiv line 120
11. def OAI.LogConcaveSampling.EulerDensity.noiseCoefficient line 125
12. lemma OAI.LogConcaveSampling.EulerDensity.scaled_standard_density line 128
13. lemma OAI.LogConcaveSampling.EulerDensity.noiseCoefficient_positive line 149
14. lemma OAI.LogConcaveSampling.EulerDensity.noiseCoefficient_finite line 154
15. theorem OAI.LogConcaveSampling.EulerDensity.joint_density line 157