OAI/Probability/LogConcave/Numerics/NodeLp.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.FinitePicard.lipschitz_zero_shift line 16
2. def OAI.LogConcaveSampling.FinitePicard.nodeLp line 22
3. lemma OAI.LogConcaveSampling.FinitePicard.nodeLp_ae line 25
4. lemma OAI.LogConcaveSampling.FinitePicard.nodeLp_lipschitz line 33
5. def OAI.LogConcaveSampling.FinitePicard.stepLp line 42
6. lemma OAI.LogConcaveSampling.FinitePicard.stepLp_lipschitz line 46
7. lemma OAI.LogConcaveSampling.FinitePicard.stepLp_ae line 51
8. theorem OAI.LogConcaveSampling.FinitePicard.rms_picard_defect line 67
9. lemma OAI.LogConcaveSampling.FinitePicard.lp_norm_sq_integral line 79
10. lemma OAI.LogConcaveSampling.FinitePicard.nodewise_rms_le line 83
11. lemma OAI.LogConcaveSampling.FinitePicard.lp_rms_eq line 110
12. lemma OAI.LogConcaveSampling.FinitePicard.iterateLp_nodes_ae line 124
13. theorem OAI.LogConcaveSampling.FinitePicard.nodes_rms line 139