OAI/Probability/LogConcave/OraclePrograms/MeanCorrect.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.OracleCompiler.MeanSize.mono line 15
2. lemma OAI.LogConcaveSampling.OracleCompiler.SampleSize.mono line 20
3. lemma OAI.LogConcaveSampling.OracleCompiler.final_mean_size line 25
4. lemma OAI.LogConcaveSampling.OracleCompiler.final_sample_size line 55
5. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.residual_pos line 85
6. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.residual_le_one line 88
7. theorem OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanTree_valid line 92
8. theorem OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleTree_valid line 133
9. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.mean_anchor_size line 178
10. structure OAI.LogConcaveSampling.OracleCompiler.MeanCorrect line 206
11. structure OAI.LogConcaveSampling.OracleCompiler.SampleCorrect line 215
12. lemma OAI.LogConcaveSampling.OracleCompiler.primitive_terminal_envelope line 225
13. lemma OAI.LogConcaveSampling.OracleCompiler.terminalMean_correct line 242
14. lemma OAI.LogConcaveSampling.OracleCompiler.terminalSample_correct line 264