OAI/Probability/LogConcave/OraclePrograms/TerminalMeanProgram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.terminalMeanProgram line 16
2. def OAI.LogConcaveSampling.terminalReservedProgram line 22
3. lemma OAI.LogConcaveSampling.terminalReservedProgram_pre_run line 30
4. abbrev OAI.LogConcaveSampling.gaussianTape line 37
5. lemma OAI.LogConcaveSampling.gaussianTape_eval line 42
6. lemma OAI.LogConcaveSampling.gaussianTape_integrable_eval line 46
7. lemma OAI.LogConcaveSampling.gaussianTape_integral_eval line 52
8. theorem OAI.LogConcaveSampling.terminalMeanProgram_squared line 56