OAI/Probability/LogConcave/Dynamics/SharedLipschitz.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LogConcaveSampling.Coupling.SquaredAt.shared_lipschitz line 15
2. lemma OAI.LogConcaveSampling.Coupling.SquaredAt.add_shared line 59
3. theorem OAI.LogConcaveSampling.Coupling.SquaredAt.mixture line 84
4. theorem OAI.LogConcaveSampling.Coupling.SquaredAt.random_anchor line 143