OAI/Probability/LogConcave/Sampling/PolynomialGrowth.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.integrable_even_norm_pow_gaussian line 16
2. lemma OAI.LogConcaveSampling.integrable_norm_pow_gaussian line 29
3. def OAI.LogConcaveSampling.HasPolynomialGrowth line 41
4. def OAI.LogConcaveSampling.HasGaussianLowerTail line 44
5. def OAI.LogConcaveSampling.tiltedIntegral line 47
6. lemma OAI.LogConcaveSampling.gaussian_tilt_bound line 51
7. lemma OAI.LogConcaveSampling.integrable_tilted line 68
8. def OAI.LogConcaveSampling.tiltDerivativeIntegrand line 85
9. lemma OAI.LogConcaveSampling.continuous_tiltDerivativeIntegrand line 88
10. lemma OAI.LogConcaveSampling.growth_tiltDerivativeIntegrand line 93
11. theorem OAI.LogConcaveSampling.hasFDerivAt_tiltedIntegral line 116
12. theorem OAI.LogConcaveSampling.contDiff_tiltedIntegral line 161