OAI/Probability/FreeIsing/Trees/ClusterColorMarginal.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem367.FiniteCluster.FiberCompatible line 18
  2. theorem OAI.Problem367.FiniteCluster.fiberCompatible_of_prescription line 21
  3. theorem OAI.Problem367.FiniteCluster.fairColor_cylinder line 27
  4. theorem OAI.Problem367.FiniteCluster.map_fairColor_cylinder line 55
  5. theorem OAI.Problem367.FiniteCluster.random_fairColor_cylinder line 71
  6. def OAI.Problem367.FiniteCluster.ClusterCompatible line 100
  7. theorem OAI.Problem367.FiniteCluster.fiberCompatible_selector_iff line 103
  8. theorem OAI.Problem367.FiniteCluster.clusterColor_cylinder line 113
  9. theorem OAI.Problem367.FiniteCluster.random_clusterColor_cylinder line 125