OAI/Probability/LogConcave/Numerics/Cost.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.MeanTree.cost line 14
2. lemma OAI.LogConcaveSampling.MeanTree.cost_anchor line 17
3. lemma OAI.LogConcaveSampling.MeanTree.cost_zero line 18
4. lemma OAI.LogConcaveSampling.MeanTree.cost_scale line 19
5. lemma OAI.LogConcaveSampling.MeanTree.cost_add line 20
6. lemma OAI.LogConcaveSampling.MeanTree.cost_mean line 23
7. lemma OAI.LogConcaveSampling.MeanTree.cost_conditional line 24
8. lemma OAI.LogConcaveSampling.MeanTree.cost_sumFin line 26
9. lemma OAI.LogConcaveSampling.MeanTree.cost_sumFamily line 30
10. theorem OAI.LogConcaveSampling.MeanTree.compileDeclared_size line 35
11. def OAI.LogConcaveSampling.MeanTree.DriftBound line 59
12. theorem OAI.LogConcaveSampling.MeanTree.compileDeclaredShift_energy_bound line 62
13. lemma OAI.LogConcaveSampling.MeanTree.sqrt_one_sub_sq_gap line 108
14. lemma OAI.LogConcaveSampling.MeanTree.mean_direct_ratio line 114
15. lemma OAI.LogConcaveSampling.MeanTree.sample_direct_ratio line 141
16. theorem OAI.LogConcaveSampling.MeanTree.exists_driftData line 152
17. lemma OAI.LogConcaveSampling.MeanTree.DirectCenter.shift line 163
18. lemma OAI.LogConcaveSampling.MeanTree.DirectCenter.mean_shift line 179
19. abbrev OAI.LogConcaveSampling.MeanTree.MeanInput line 211
20. abbrev OAI.LogConcaveSampling.MeanTree.SampleInput line 212
21. def OAI.LogConcaveSampling.MeanTree.meanInputMove line 214
22. def OAI.LogConcaveSampling.MeanTree.sampleInputMove line 216
23. def OAI.LogConcaveSampling.MeanTree.literalMean line 219
24. def OAI.LogConcaveSampling.MeanTree.literalSample line 225
25. lemma OAI.LogConcaveSampling.MeanTree.literalMean_geometry line 230
26. lemma OAI.LogConcaveSampling.MeanTree.literalSample_geometry line 239
27. theorem OAI.LogConcaveSampling.MeanTree.literalMean_drift line 250
28. theorem OAI.LogConcaveSampling.MeanTree.literalSample_drift line 266