OAI/Probability/LogConcave/Sampling/AverageLipschitz.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.zero_average_lipschitz line 14
2. lemma OAI.LogConcaveSampling.proximal_iterate_lipschitz line 28
3. lemma OAI.LogConcaveSampling.proximal_iterate_smoothing line 44
4. theorem OAI.LogConcaveSampling.proximal_chain_mixing line 62
5. lemma OAI.LogConcaveSampling.proximal_chain_observable line 105
6. lemma OAI.LogConcaveSampling.TVAtMost.cap_one line 125
7. lemma OAI.LogConcaveSampling.proximal_local_cap_lipschitz line 133
8. theorem OAI.LogConcaveSampling.proximal_chain_perturbation line 145