OAI/Probability/LogConcave/Sampling/TiltedExpectation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.growth_const line 16
2. lemma OAI.LogConcaveSampling.tilted_partition_pos line 22
3. def OAI.LogConcaveSampling.tiltedExpectation line 29
4. theorem OAI.LogConcaveSampling.contDiff_tiltedExpectation line 33
5. theorem OAI.LogConcaveSampling.hasFDerivAt_tiltedExpectation line 42
6. lemma OAI.LogConcaveSampling.Primitive.hasGaussianLowerTail line 64
7. lemma OAI.LogConcaveSampling.growth_of_lipschitz line 82
8. theorem OAI.LogConcaveSampling.Primitive.contDiff_tilted_mean line 92