OAI/Probability/FreeIsing/Trees/CutLevelBranchIndependence.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.RootedBroadcast.strictDescendant_length_gt line 19
  2. theorem OAI.Problem367.RootedBroadcast.cutLevel_descendants_disjoint line 28
  3. theorem OAI.Problem367.RootedBroadcast.cutLevel_strictDescendants_disjoint line 39
  4. def OAI.Problem367.RootedBroadcast.cutUpperExtension line 47
  5. theorem OAI.Problem367.RootedBroadcast.measurable_cutUpperExtension line 50
  6. def OAI.Problem367.RootedBroadcast.cutSpins line 60
  7. theorem OAI.Problem367.RootedBroadcast.measurable_cutSpins line 64
  8. theorem OAI.Problem367.RootedBroadcast.cutSpins_upper_extension line 69
  9. def OAI.Problem367.RootedBroadcast.cutLabels line 79
  10. theorem OAI.Problem367.RootedBroadcast.measurable_cutLabels line 83
  11. theorem OAI.Problem367.RootedBroadcast.indepFun_cutSpins_cutLabels line 87
  12. theorem OAI.Problem367.RootedBroadcast.map_cutSpins_cutLabels line 115
  13. theorem OAI.Problem367.RootedBroadcast.iCondIndepFun_factor_cutLevel line 127
  14. theorem OAI.Problem367.freeIsingMeasure_iCondIndepFun_cutLevel line 172
  15. theorem OAI.Problem367.HasFreeIsingLaw.iCondIndepFun_cutLevel line 197