OAI/Probability/LogConcave/Numerics/Correction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.FinitePicard.correction line 14
2. def OAI.LogConcaveSampling.FinitePicard.step line 17
3. lemma OAI.LogConcaveSampling.FinitePicard.correction_lipschitz line 20
4. lemma OAI.LogConcaveSampling.FinitePicard.step_lipschitz line 42
5. theorem OAI.LogConcaveSampling.FinitePicard.iterate_defect line 49
6. def OAI.LogConcaveSampling.FinitePicard.nodes line 65
7. lemma OAI.LogConcaveSampling.FinitePicard.nodes_eq_iterate line 70
8. theorem OAI.LogConcaveSampling.FinitePicard.nodes_lipschitz line 76
9. theorem OAI.LogConcaveSampling.FinitePicard.nodes_correction_lipschitz line 87