OAI/Probability/LogConcave/OraclePrograms/StandaloneCorrect.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.OracleCompiler.StandaloneCorrect line 15
2. def OAI.LogConcaveSampling.OracleCompiler.UniformAccuracy line 20
3. lemma OAI.LogConcaveSampling.OracleCompiler.sourceA_pos line 29
4. lemma OAI.LogConcaveSampling.OracleCompiler.childSizes_positive line 35
5. lemma OAI.LogConcaveSampling.OracleCompiler.uniformAccuracy_terminal line 51
6. theorem OAI.LogConcaveSampling.OracleCompiler.uniform_routine_accuracy line 77
7. theorem OAI.LogConcaveSampling.calibrated_sample_circuit_order line 250