OAI/Probability/SpanningForest/GraphTreePosteriorEquiv.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Problem336.GraphTreePosterior.energy_eq_pairFieldline 12 - theorem
OAI.Problem336.GraphTreePosterior.mean_eq_weightedTreeline 27 - theorem
OAI.Problem336.GraphTreePosterior.observed_pairs_relabelline 39 - theorem
OAI.Problem336.GraphTreePosterior.mean_relabelline 48 - theorem
OAI.Problem336.GraphTreePosterior.edgeCodes_relabelline 60 - theorem
OAI.Problem336.GraphTreePosterior.finiteBallMean_relabelline 78 - theorem
OAI.Problem336.GraphTreePosterior.innerMean_relabelline 89 - theorem
OAI.Problem336.GraphTreePosterior.drift_relabelline 95