OAI/Probability/LogConcave/Sampling/ConditionalMeanArray.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.scoreAugmented_gaussian line 13
2. lemma OAI.LogConcaveSampling.scoreField_gaussian_allSplit line 37
3. lemma OAI.LogConcaveSampling.centeringScore_allSplit line 54
4. lemma OAI.LogConcaveSampling.probability_gibbs_of_gaussianTail line 81
5. def OAI.LogConcaveSampling.conditionalMeanArray line 89
6. lemma OAI.LogConcaveSampling.conditionalMeanArray_polySmooth line 93
7. lemma OAI.LogConcaveSampling.conditionalMeanArray_allSplit line 99
8. lemma OAI.LogConcaveSampling.conditionalMeanArray_energy line 137
9. lemma OAI.LogConcaveSampling.directional_basis_gradient line 161
10. lemma OAI.LogConcaveSampling.gradient_productPotential line 168
11. lemma OAI.LogConcaveSampling.productPointEquiv_fst_norm_le line 180
12. lemma OAI.LogConcaveSampling.productPointEquiv_snd_norm_le line 184
13. lemma OAI.LogConcaveSampling.productPotential_gradient_lipschitz line 189