OAI/Probability/LogConcave/Sampling/PrimitiveField.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.conditionalLaw_hasExpMoments line 19
2. def OAI.LogConcaveSampling.primitiveField line 41
3. abbrev OAI.LogConcaveSampling.JointPoint line 44
4. def OAI.LogConcaveSampling.jointImage line 46
5. lemma OAI.LogConcaveSampling.jointImage_norm_sq line 49
6. lemma OAI.LogConcaveSampling.jointImage_contDiff line 53
7. lemma OAI.LogConcaveSampling.jointImage_lipschitz line 58
8. lemma OAI.LogConcaveSampling.primitiveField_contDiff line 79
9. lemma OAI.LogConcaveSampling.primitiveField_lipschitz line 84
10. def OAI.LogConcaveSampling.jointConditionalLaw line 94
11. lemma OAI.LogConcaveSampling.jointConditionalLaw_properties line 98