OAI/Probability/LogConcave/Analysis/GibbsOpenPos.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.LogConcaveSampling.gibbs_openPosline 13 - lemma
OAI.LogConcaveSampling.directional_adjoint_basisline 23 - theorem
OAI.LogConcaveSampling.stein_weak_to_strongline 33 - theorem
OAI.LogConcaveSampling.centeringKernel_strongline 68