OAI/Probability/LogConcave/OraclePrograms/PairDistBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.pair_dist_bounds line 18
2. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanTree_anchorVariation line 25
3. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleTree_anchorVariation line 40
4. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanTree_anchor_lipschitz line 58
5. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleTree_anchor_lipschitz line 76
6. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanCompiled_anchor_lipschitz line 95
7. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleCompiled_anchor_lipschitz line 123
8. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanTree_eval line 166
9. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleTree_eval line 175
10. theorem OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanTree_numerical line 185
11. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanTree_numerical_noisy line 223