OAI/Probability/LogConcave/Analysis/ConditionalPotential.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.HasGaussianLowerTail.hasExpMoments line 20
2. lemma OAI.LogConcaveSampling.Primitive.hasExpMoments line 42
3. lemma OAI.LogConcaveSampling.Appell.HasExpMoments.map_lipschitz line 48
4. theorem OAI.LogConcaveSampling.gibbs_map_equiv line 78
5. lemma OAI.LogConcaveSampling.gibbs_map_smul line 101
6. lemma OAI.LogConcaveSampling.gibbs_map_add line 116
7. lemma OAI.LogConcaveSampling.gibbs_map_affine line 130
8. def OAI.LogConcaveSampling.conditionalPotential line 144
9. lemma OAI.LogConcaveSampling.probability_time line 148
10. lemma OAI.LogConcaveSampling.conditionalPotential_pullback line 154
11. lemma OAI.LogConcaveSampling.conditionalLaw_map line 169
12. lemma OAI.LogConcaveSampling.conditional_smallness line 180
13. lemma OAI.LogConcaveSampling.conditionalLaw_probability line 190
14. lemma OAI.LogConcaveSampling.conditionalLaw_hasPoincare line 205