OAI/Probability/LogConcave/Sampling/JointPosition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.jointPosition line 21
2. def OAI.LogConcaveSampling.jointField line 24
3. lemma OAI.LogConcaveSampling.jointPair_inner line 27
4. lemma OAI.LogConcaveSampling.jointPosition_inner line 35
5. lemma OAI.LogConcaveSampling.jointField_inner line 41
6. lemma OAI.LogConcaveSampling.jointPosition_basis line 47
7. lemma OAI.LogConcaveSampling.jointField_basis line 60
8. lemma OAI.LogConcaveSampling.joint_laplace_one line 73
9. lemma OAI.LogConcaveSampling.joint_normalizedLaplace line 83