OAI/Probability/LogConcave/Numerics/Forward.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.MeanTree.forward line 15
2. lemma OAI.LogConcaveSampling.MeanTree.eval_forward line 21
3. lemma OAI.LogConcaveSampling.MeanTree.depth_forward line 37
4. def OAI.LogConcaveSampling.sampleMeanCircuit line 46
5. def OAI.LogConcaveSampling.samplingEnvelope line 50
6. theorem OAI.LogConcaveSampling.sampleMeanCircuit_rms line 53
7. def OAI.LogConcaveSampling.MeanTree.oriented line 125
8. lemma OAI.LogConcaveSampling.MeanTree.oriented_zero line 129
9. def OAI.LogConcaveSampling.MeanTree.DirectCenter line 132
10. lemma OAI.LogConcaveSampling.MeanTree.conditional_centers_direct line 136
11. lemma OAI.LogConcaveSampling.MeanTree.probability_centers_direct line 145
12. lemma OAI.LogConcaveSampling.MeanTree.forward_centers_direct line 161
13. lemma OAI.LogConcaveSampling.MeanTree.harmonic_centers_direct line 177
14. lemma OAI.LogConcaveSampling.MeanTree.kernelCorrection_centers_direct line 203
15. lemma OAI.LogConcaveSampling.MeanTree.kernelQuadrature_centers_direct line 235
16. lemma OAI.LogConcaveSampling.MeanTree.pairPicard_shape line 272
17. lemma OAI.LogConcaveSampling.MeanTree.velocity_centers_direct line 294
18. lemma OAI.LogConcaveSampling.MeanTree.centeringStates_centers_direct line 321
19. lemma OAI.LogConcaveSampling.MeanTree.meanCircuit_centers_direct line 340