OAI/Probability/LogConcave/Analysis/Poincare.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.HasPoincare line 20
2. lemma OAI.LogConcaveSampling.derivative_comp_lipschitz_bound line 32
3. theorem OAI.LogConcaveSampling.HasPoincare.map line 42
4. lemma OAI.LogConcaveSampling.HasPoincare.mono line 70
5. lemma OAI.LogConcaveSampling.HasPoincare.lipschitz_variance line 76
6. theorem OAI.LogConcaveSampling.Primitive.hasPoincare line 96