OAI/Probability/FreeIsing/Trees/ClusterFactorMap.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem367.ClusterFactorMap.Input line 17
  2. def OAI.Problem367.ClusterFactorMap.relabelInput line 20
  3. def OAI.Problem367.ClusterFactorMap.openAdj line 23
  4. def OAI.Problem367.ClusterFactorMap.connected line 26
  5. def OAI.Problem367.ClusterFactorMap.factor line 29
  6. lemma OAI.Problem367.ClusterFactorMap.factor_apply line 32
  7. lemma OAI.Problem367.ClusterFactorMap.openAdj_edge_iff line 36
  8. lemma OAI.Problem367.ClusterFactorMap.measurable_relabelInput line 40
  9. lemma OAI.Problem367.ClusterFactorMap.openAdj_sub_treeAdj line 45
  10. lemma OAI.Problem367.ClusterFactorMap.openAdj_symmetric line 48
  11. lemma OAI.Problem367.ClusterFactorMap.connected_equivalence line 55
  12. lemma OAI.Problem367.ClusterFactorMap.openAdj_relabel line 63
  13. lemma OAI.Problem367.ClusterFactorMap.connected_relabel line 69
  14. lemma OAI.Problem367.ClusterFactorMap.connected_relabel_eq line 75
  15. theorem OAI.Problem367.ClusterFactorMap.factor_relabel line 83
  16. theorem OAI.Problem367.ClusterFactorMap.factor_eq_of_connected line 98
  17. theorem OAI.Problem367.ClusterFactorMap.factor_eq_at_minimum line 104
  18. lemma OAI.Problem367.ClusterFactorMap.measurableSet_openAdj line 110
  19. lemma OAI.Problem367.ClusterFactorMap.measurableSet_connected line 120
  20. theorem OAI.Problem367.ClusterFactorMap.measurable_factor line 124