OAI/Probability/LogConcave/OraclePrograms/TerminalMean.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.SeedCompiler.terminalMean line 20
2. def OAI.LogConcaveSampling.SeedCompiler.terminalSample line 25
3. lemma OAI.LogConcaveSampling.SeedCompiler.terminalMean_run line 31
4. lemma OAI.LogConcaveSampling.SeedCompiler.terminalSample_run line 37
5. def OAI.LogConcaveSampling.SeedCompiler.terminalShift line 44
6. lemma OAI.LogConcaveSampling.SeedCompiler.terminalShift_energy line 46
7. lemma OAI.LogConcaveSampling.SeedCompiler.terminalQuery_invariant line 49
8. lemma OAI.LogConcaveSampling.SeedCompiler.terminalMean_shift line 55
9. lemma OAI.LogConcaveSampling.SeedCompiler.terminalSample_shift line 61
10. lemma OAI.LogConcaveSampling.SeedCompiler.terminalMean_history_shift line 70
11. lemma OAI.LogConcaveSampling.SeedCompiler.terminalSample_history_shift line 77
12. theorem OAI.LogConcaveSampling.SeedCompiler.restored_from_joint_law line 103
13. theorem OAI.LogConcaveSampling.SeedCompiler.restored_error_integral line 121