OAI/Probability/LogConcave/Sampling/PrependTape.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.oneSlot_preserving line 18
2. def OAI.LogConcaveSampling.prependTape line 26
3. lemma OAI.LogConcaveSampling.prependTape_preserving line 29
4. def OAI.LogConcaveSampling.meanTape line 35
5. lemma OAI.LogConcaveSampling.meanTape_preserving line 38
6. lemma OAI.LogConcaveSampling.sampleParent_run_prepend line 45
7. lemma OAI.LogConcaveSampling.meanParent_run_meanTape line 52
8. theorem OAI.LogConcaveSampling.sampleParent_squared line 76
9. theorem OAI.LogConcaveSampling.meanParent_squared line 138