OAI/Probability/LogConcave/LowerBounds/CouplingNoise.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LogConcaveSampling.LowerBound.CouplingNoise line 19
2. def OAI.LogConcaveSampling.LowerBound.couplingLaw line 22
3. instance OAI.LogConcaveSampling.LowerBound.couplingLaw_probability line 27
4. def OAI.LogConcaveSampling.LowerBound.couplingState line 31
5. lemma OAI.LogConcaveSampling.LowerBound.measurable_couplingState line 36
6. lemma OAI.LogConcaveSampling.LowerBound.couplingState_law line 43
7. theorem OAI.LogConcaveSampling.LowerBound.coupling_complete_law line 62
8. lemma OAI.LogConcaveSampling.LowerBound.revealRun_tape line 75
9. def OAI.LogConcaveSampling.LowerBound.couplingColumns line 93
10. lemma OAI.LogConcaveSampling.LowerBound.measurable_couplingColumns line 97
11. lemma OAI.LogConcaveSampling.LowerBound.tapeHull_le_couplingColumns line 106
12. theorem OAI.LogConcaveSampling.LowerBound.coupling_output_span line 120
13. theorem OAI.LogConcaveSampling.LowerBound.coupling_output_correct line 156