OAI/Probability/FreeIsing/Trees/WeightEncoding.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Problem367.ConnectedFinset.prod_inducedEdges_eq_parent_prodline 10 - lemma
OAI.Problem367.ConnectedFinset.freeCylinderWeight_eq_parent_prodline 25 - def
OAI.Problem367.treeNoiseMassline 37 - lemma
OAI.Problem367.treeNoiseMass_sumline 40 - lemma
OAI.Problem367.treeNoiseMass_nonnegline 52 - lemma
OAI.Problem367.treeNoiseMass_le_oneline 60 - lemma
OAI.Problem367.treeNoiseMass_prod_sumline 68 - lemma
OAI.Problem367.ConnectedFinset.freeCylinderWeight_eq_noise_prodline 75