OAI/Probability/FreeIsing/Trees/FiniteClusterLaw.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.FiniteCluster.Compatible line 16
  2. def OAI.Problem367.FiniteCluster.bondWeight line 19
  3. def OAI.Problem367.FiniteCluster.colorWeight line 22
  4. lemma OAI.Problem367.FiniteCluster.bondWeight_nonneg line 25
  5. lemma OAI.Problem367.FiniteCluster.colorWeight_nonneg line 30
  6. lemma OAI.Problem367.FiniteCluster.bondWeight_sum line 35
  7. lemma OAI.Problem367.FiniteCluster.weighted_color_eq line 40
  8. theorem OAI.Problem367.FiniteCluster.marginal_eq_edge_product line 52
  9. theorem OAI.Problem367.FiniteCluster.colorWeight_eq_vertices_sub_edges line 65
  10. theorem OAI.Problem367.FiniteCluster.marginal_eq_freeCylinderWeight line 80
  11. theorem OAI.Problem367.FiniteCluster.colorWeight_eq_edge_product line 88
  12. theorem OAI.Problem367.FiniteCluster.colorWeight_sum line 113