OAI/Probability/LogConcave/Sampling/ConditionalMeanScalar.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.integral_gibbs_add_const line 21
2. lemma OAI.LogConcaveSampling.HasGaussianLowerTail.integrable_exp line 34
3. lemma OAI.LogConcaveSampling.HasGaussianLowerTail.comp_inverse_affine line 40
4. lemma OAI.LogConcaveSampling.normalizedLaplace_gibbs line 59
5. lemma OAI.LogConcaveSampling.conditionalPotential_continuous line 85
6. lemma OAI.LogConcaveSampling.conditional_hasGaussianLowerTail line 90
7. lemma OAI.LogConcaveSampling.conditionalPotential_shift line 102
8. def OAI.LogConcaveSampling.conditionalMeanScalar line 113
9. theorem OAI.LogConcaveSampling.conditionalMeanScalar_shift line 116
10. theorem OAI.LogConcaveSampling.conditionalMeanScalar_smooth line 141