OAI/Probability/LogConcave/Numerics/CentersBoundPicard.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.MeanTree.centersBound_picard line 14
2. lemma OAI.LogConcaveSampling.MeanTree.probability_weights line 30
3. lemma OAI.LogConcaveSampling.MeanTree.harmonic_weights line 55
4. lemma OAI.LogConcaveSampling.MeanTree.kernelCorrection_weights line 86
5. lemma OAI.LogConcaveSampling.MeanTree.kernelQuadrature_weights line 149
6. lemma OAI.LogConcaveSampling.MeanTree.velocity_weights line 184
7. lemma OAI.LogConcaveSampling.MeanTree.weight_velocity_input_independent line 225
8. lemma OAI.LogConcaveSampling.MeanTree.velocity_root_weights line 233
9. lemma OAI.LogConcaveSampling.MeanTree.pairPicard_weights line 249
10. lemma OAI.LogConcaveSampling.MeanTree.centersBound_pairPicard line 269
11. theorem OAI.LogConcaveSampling.MeanTree.centeringStates_weights line 300
12. theorem OAI.LogConcaveSampling.MeanTree.meanCircuit_weights line 328