OAI/Probability/LogConcave/Dynamics/Squared.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LogConcaveSampling.Coupling.exists_countable_quantizer line 15
2. def OAI.LogConcaveSampling.Coupling.SquaredAt line 23
3. theorem OAI.LogConcaveSampling.Coupling.measurable_coupling_of_pointwise line 28
4. def OAI.LogConcaveSampling.Coupling.lift line 89
5. instance OAI.LogConcaveSampling.Coupling.lift_probability line 93
6. lemma OAI.LogConcaveSampling.Coupling.lift_fst line 97
7. theorem OAI.LogConcaveSampling.Coupling.lift_map line 101
8. lemma OAI.LogConcaveSampling.Coupling.lift_integrable line 116
9. theorem OAI.LogConcaveSampling.Coupling.absorb_coupling line 143
10. theorem OAI.LogConcaveSampling.Coupling.SquaredAt.of_joint line 256
11. lemma OAI.LogConcaveSampling.Coupling.SquaredAt.mono line 276
12. lemma OAI.LogConcaveSampling.Coupling.SquaredAt.nonneg line 281
13. lemma OAI.LogConcaveSampling.Coupling.SquaredAt.lipschitz line 286
14. lemma OAI.LogConcaveSampling.Coupling.SquaredAt.reindex line 306