OAI/Probability/LogConcave/LowerBounds/DensityCoefficient.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.LowerBound.targetVariance_ne_zero line 28
2. def OAI.LogConcaveSampling.LowerBound.densityCoefficient line 34
3. lemma OAI.LogConcaveSampling.LowerBound.gaussianPDF_targetVariance line 37
4. lemma OAI.LogConcaveSampling.LowerBound.targetGaussian_density line 49
5. lemma OAI.LogConcaveSampling.LowerBound.quadraticPotential_eq_spectral line 72
6. theorem OAI.LogConcaveSampling.LowerBound.quadratic_gibbs_eq_gaussian line 86