OAI/Probability/LogConcave/Numerics/NodesContinuous.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.LogConcaveSampling.FinitePicard.nodes_continuousline 14 - lemma
OAI.LogConcaveSampling.probabilityAnchored_continuousline 27 - theorem
OAI.LogConcaveSampling.probabilityAnchored_marginal_rmsline 39 - theorem
OAI.LogConcaveSampling.harmonicPicard_stationary_rmsline 95