OAI/Probability/LogConcave/Dynamics/DistanceCoupled.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.Coupling.DistanceCoupled line 15
2. lemma OAI.LogConcaveSampling.Coupling.tight_range_of_tendsto line 19
3. theorem OAI.LogConcaveSampling.Coupling.distanceCoupled_of_tendsto line 29
4. lemma OAI.LogConcaveSampling.Coupling.DistanceCoupled.squared line 87