OAI/Probability/LogConcave/LowerBounds/RoundFrames.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.LowerBound.roundFrames line 20
2. lemma OAI.LogConcaveSampling.LowerBound.measurable_inverse_frameTransport line 27
3. lemma OAI.LogConcaveSampling.LowerBound.measurable_roundFrames line 34
4. lemma OAI.LogConcaveSampling.LowerBound.filledForward_law line 53
5. theorem OAI.LogConcaveSampling.LowerBound.roundFrames_law line 73
6. lemma OAI.LogConcaveSampling.LowerBound.roundFrames_compatible line 104
7. def OAI.LogConcaveSampling.LowerBound.linearReply line 117
8. lemma OAI.LogConcaveSampling.LowerBound.measurable_linearReply line 122
9. def OAI.LogConcaveSampling.LowerBound.roundCoordinate line 128
10. lemma OAI.LogConcaveSampling.LowerBound.measurable_roundCoordinate line 131
11. lemma OAI.LogConcaveSampling.LowerBound.roundCoordinate_mem line 141
12. lemma OAI.LogConcaveSampling.LowerBound.replyCoordinate_mem line 147
13. theorem OAI.LogConcaveSampling.LowerBound.roundReply_correct line 152
14. theorem OAI.LogConcaveSampling.LowerBound.roundFrames_span_growth line 171