OAI/Probability/LogConcave/Sampling/PosteriorJointIntegral.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.LogConcaveSampling.posterior_joint_integral_zeroline 14 - lemma
OAI.LogConcaveSampling.posterior_reconstruction_integralline 61