OAI/Probability/FreeIsing/Trees/EncodedClusterLaw.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem367.EncodedClusterLaw.Environment line 17
  2. def OAI.Problem367.EncodedClusterLaw.codedBond line 20
  3. theorem OAI.Problem367.EncodedClusterLaw.measurable_codedBond line 24
  4. def OAI.Problem367.EncodedClusterLaw.inducedEdge line 31
  5. theorem OAI.Problem367.EncodedClusterLaw.inducedEdge_injective line 36
  6. theorem OAI.Problem367.EncodedClusterLaw.measurePreserving_single_edge line 42
  7. theorem OAI.Problem367.EncodedClusterLaw.iIndepFun_coded_edges line 48
  8. theorem OAI.Problem367.EncodedClusterLaw.iIndepFun_codedBond line 62
  9. theorem OAI.Problem367.EncodedClusterLaw.codedBond_true line 69
  10. theorem OAI.Problem367.EncodedClusterLaw.codedBond_false line 80
  11. def OAI.Problem367.EncodedClusterLaw.productFactor line 91
  12. theorem OAI.Problem367.EncodedClusterLaw.measurable_productFactor line 95
  13. theorem OAI.Problem367.EncodedClusterLaw.hasFreeIsingLaw_productFactor_of_colorLaw line 101
  14. theorem OAI.Problem367.EncodedClusterLaw.hasFreeIsingLaw_factor_of_colorLaw line 120
  15. def OAI.Problem367.EncodedClusterLaw.environmentRelation line 143
  16. theorem OAI.Problem367.EncodedClusterLaw.openMask_eq_filter line 147
  17. theorem OAI.Problem367.EncodedClusterLaw.colorLaw_of_ae_finite line 157
  18. theorem OAI.Problem367.EncodedClusterLaw.hasFreeIsingLaw_factor_of_ae_finite line 178