OAI/Probability/LogConcave/OraclePrograms/MeanSize.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.OracleCompiler.MeanSize line 15
2. def OAI.LogConcaveSampling.OracleCompiler.SampleSize line 18
3. lemma OAI.LogConcaveSampling.OracleCompiler.MeanSize.nonneg line 21
4. lemma OAI.LogConcaveSampling.OracleCompiler.SampleSize.nonneg line 23
5. lemma OAI.LogConcaveSampling.OracleCompiler.internal_meanSize line 27
6. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanCenterBudget_small line 53
7. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleCenterBudget_small line 60
8. def OAI.LogConcaveSampling.OracleCompiler.fixedProbabilityBudget line 84
9. def OAI.LogConcaveSampling.OracleCompiler.fixedHarmonicBudget line 87
10. def OAI.LogConcaveSampling.OracleCompiler.fixedCenteringBudget line 90
11. lemma OAI.LogConcaveSampling.OracleCompiler.fixedProbabilityBudget_spec line 94
12. lemma OAI.LogConcaveSampling.OracleCompiler.fixedCenteringBudget_spec line 99
13. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.quadratureBudget line 116
14. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.derivativeBudget line 117
15. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.actualA line 118
16. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.actualAf line 121
17. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.actualA_pos line 123
18. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.actualAf_pos line 130
19. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.angle_mem line 136
20. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanTree_actual_weights line 146
21. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleTree_actual_weights line 182