OAI/Probability/LogConcave/Sampling/Primitive.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LogConcaveSampling.quadratic_bounds_on_segment line 16
2. theorem OAI.LogConcaveSampling.hessian_bounds_of_gradient_lipschitz line 47
3. theorem OAI.LogConcaveSampling.quadratic_remainder_of_gradient_lipschitz line 57
4. structure OAI.LogConcaveSampling.Primitive line 70
5. def OAI.LogConcaveSampling.primitivePotential line 74
6. def OAI.LogConcaveSampling.modeStep line 77
7. def OAI.LogConcaveSampling.modeIterates line 80
8. theorem OAI.LogConcaveSampling.modeStep_lipschitz line 83
9. theorem OAI.LogConcaveSampling.exists_mode_with_iteration_bound line 97