OAI/Probability/LogConcave/OraclePrograms/ReservedProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.LogConcaveSampling.OracleCompiler.ReservedProgram line 15
2. def OAI.LogConcaveSampling.OracleCompiler.ReservedProgram.full line 24
3. lemma OAI.LogConcaveSampling.OracleCompiler.ReservedProgram.full_run line 32
4. def OAI.LogConcaveSampling.OracleCompiler.ReservedProgram.extraShift line 41
5. lemma OAI.LogConcaveSampling.OracleCompiler.ReservedProgram.full_equivariant line 44
6. lemma OAI.LogConcaveSampling.OracleCompiler.ReservedProgram.extraShift_energy line 62
7. def OAI.LogConcaveSampling.OracleCompiler.sampleParent line 67
8. lemma OAI.LogConcaveSampling.OracleCompiler.sampleParent_run line 76
9. def OAI.LogConcaveSampling.OracleCompiler.meanParent line 84
10. lemma OAI.LogConcaveSampling.OracleCompiler.meanParent_run line 96
11. lemma OAI.LogConcaveSampling.OracleCompiler.meanParent_shift_energy line 105
12. lemma OAI.LogConcaveSampling.OracleCompiler.sampleParent_shift_energy line 112
13. lemma OAI.LogConcaveSampling.OracleCompiler.mean_anchor_shift_identity line 118