OAI/Probability/LogConcave/Numerics/ReanchorWeight.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.FinitePicard.reanchorWeight line 15
2. lemma OAI.LogConcaveSampling.FinitePicard.reanchorWeight_budget line 17
3. lemma OAI.LogConcaveSampling.FinitePicard.step_reanchor_defect line 24
4. lemma OAI.LogConcaveSampling.FinitePicard.integral_norm_sub_sq_bound line 32
5. def OAI.LogConcaveSampling.probabilityAnchoredPicard line 59
6. lemma OAI.LogConcaveSampling.probabilityAnchored_lipschitz line 65
7. theorem OAI.LogConcaveSampling.probabilityAnchored_rms line 88