OAI/Probability/LogConcave/Sampling/TapeSnocEquiv.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.probability_measure_eq_of_subsingleton line 20
2. def OAI.LogConcaveSampling.tapeSnocEquiv line 34
3. lemma OAI.LogConcaveSampling.tapeSnocEquiv_apply line 39
4. def OAI.LogConcaveSampling.seedTapeSnoc line 44
5. lemma OAI.LogConcaveSampling.seedTapeSnoc_apply line 48
6. lemma OAI.LogConcaveSampling.seedTapeSnoc_law line 54
7. def OAI.LogConcaveSampling.stateRun line 74
8. lemma OAI.LogConcaveSampling.stateRun_snoc line 80
9. lemma OAI.LogConcaveSampling.measurable_stateRun line 86
10. lemma OAI.LogConcaveSampling.stateRun_law line 97
11. lemma OAI.LogConcaveSampling.stateRun_ae_invariant line 119