OAI/Probability/LogConcave/Numerics/CenteringVelocityPicard.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LogConcaveSampling.kernelQuadraturePicard_full_rms line 13
2. def OAI.LogConcaveSampling.centeringVelocityPicard line 73
3. lemma OAI.LogConcaveSampling.velocity_scale_cancel line 80
4. theorem OAI.LogConcaveSampling.centeringVelocityPicard_lipschitz line 87
5. lemma OAI.LogConcaveSampling.centeringVelocityPicard_lipschitz_coefficient line 125