OAI/Probability/LogConcave/Sampling/CenteringVelocityJoint.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.productPointEquiv_lipschitz_one line 12
2. lemma OAI.LogConcaveSampling.productPointEquiv_symm_norm_le line 20
3. lemma OAI.LogConcaveSampling.productPointEquiv_symm_lipschitz_two line 30
4. lemma OAI.LogConcaveSampling.centering_joint_product_law line 37
5. def OAI.LogConcaveSampling.centeringVelocityJoint line 60
6. lemma OAI.LogConcaveSampling.actual_centering_joint_field line 66
7. lemma OAI.LogConcaveSampling.centeringVelocityJoint_error_sq line 80
8. lemma OAI.LogConcaveSampling.centeringVelocityJoint_rms_of_kernel line 99