OAI/Probability/LogConcave/LowerBounds/TranscriptRejection.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.transcriptRejection line 20
2. lemma OAI.LogConcaveSampling.measurable_transcriptRejection line 28
3. lemma OAI.LogConcaveSampling.transcriptRejection_eq line 44
4. def OAI.LogConcaveSampling.finiteRejectionAlgorithm line 54
5. lemma OAI.LogConcaveSampling.finiteRejection_history line 61
6. lemma OAI.LogConcaveSampling.finiteRejection_run line 77
7. lemma OAI.LogConcaveSampling.rejection_failure_bound line 87
8. theorem OAI.LogConcaveSampling.finite_dimension_sampler line 100
9. abbrev OAI.LogConcaveSampling.LowerBound.Rotations line 144
10. theorem OAI.LogConcaveSampling.LowerBound.orthogonal_entry_bound line 146
11. theorem OAI.LogConcaveSampling.LowerBound.orthogonal_group_isCompact line 158
12. instance OAI.LogConcaveSampling.LowerBound.rotations_compactSpace line 170
13. instance OAI.LogConcaveSampling.LowerBound.rotations_measurableSpace line 173
14. instance OAI.LogConcaveSampling.LowerBound.rotations_borelSpace line 174
15. instance OAI.LogConcaveSampling.LowerBound.rotations_secondCountable line 176
16. instance OAI.LogConcaveSampling.LowerBound.rotations_measurableMul line 182
17. def OAI.LogConcaveSampling.LowerBound.rotationHaar line 185
18. instance OAI.LogConcaveSampling.LowerBound.rotationHaar_probability line 188
19. instance OAI.LogConcaveSampling.LowerBound.rotationHaar_isHaar line 192