OAI/Probability/LogConcave/Sampling/CenteringJointLaw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.centering_joint_law line 13
2. lemma OAI.LogConcaveSampling.centering_position_law line 24
3. lemma OAI.LogConcaveSampling.harmonic_position_law line 34
4. lemma OAI.LogConcaveSampling.rms_bound_pullback line 45