OAI/Probability/LogConcave/Sampling/QuadraticExpectation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.integral_gibbs_vector line 20
2. lemma OAI.LogConcaveSampling.integral_gibbs_add_const_vector line 31
3. def OAI.LogConcaveSampling.quadraticExpectation line 43
4. lemma OAI.LogConcaveSampling.quadratic_partition_pos line 47
5. lemma OAI.LogConcaveSampling.contDiffAt_quadraticExpectation line 55
6. def OAI.LogConcaveSampling.conditionalParameter line 65
7. lemma OAI.LogConcaveSampling.conditionalPotential_quadratic line 68
8. lemma OAI.LogConcaveSampling.conditional_integral_quadratic line 82
9. lemma OAI.LogConcaveSampling.conditionalParameter_smooth line 107
10. theorem OAI.LogConcaveSampling.conditionalFieldMean_joint_smooth line 117