OAI/Probability/LogConcave/Analysis/PoincareVectorVariance.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LogConcaveSampling.poincare_vector_variance line 13
2. theorem OAI.LogConcaveSampling.poincare_sq_norm_center line 51
3. lemma OAI.LogConcaveSampling.stdGaussian_sq_norm line 58
4. lemma OAI.LogConcaveSampling.poincare_integral_norm_center_sharp line 89
5. lemma OAI.LogConcaveSampling.conditionalFieldMean_center_error_sharp line 110
6. lemma OAI.LogConcaveSampling.conditionalFieldMean_center_zero_bound line 125