OAI/Probability/FreeIsing/Trees/RootedBroadcastLaw.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.RootedBroadcast.root line 15
  2. lemma OAI.Problem367.RootedBroadcast.root_val line 17
  3. lemma OAI.Problem367.RootedBroadcast.eq_root_iff line 19
  4. def OAI.Problem367.RootedBroadcast.eraseRootNoise line 27
  5. lemma OAI.Problem367.RootedBroadcast.ofNoise_root_decomposition line 30
  6. abbrev OAI.Problem367.RootedBroadcast.NonrootVertex line 52
  7. def OAI.Problem367.RootedBroadcast.nonrootNoise line 54
  8. lemma OAI.Problem367.RootedBroadcast.measurable_nonrootNoise line 57
  9. def OAI.Problem367.RootedBroadcast.rootlessFactor line 66
  10. lemma OAI.Problem367.RootedBroadcast.measurable_rootlessFactor line 69
  11. lemma OAI.Problem367.RootedBroadcast.factor_root_decomposition line 72
  12. lemma OAI.Problem367.RootedBroadcast.factor_edge_agreement line 88
  13. lemma OAI.Problem367.RootedBroadcast.factor_cylinder_event line 102
  14. def OAI.Problem367.RootedBroadcast.edgeVertex line 120
  15. lemma OAI.Problem367.RootedBroadcast.edgeVertex_injective line 129
  16. lemma OAI.Problem367.RootedBroadcast.nonroot_edge_event_mass line 136
  17. lemma OAI.Problem367.RootedBroadcast.freeCylinderWeight_eq_edge_product line 170
  18. lemma OAI.Problem367.RootedBroadcast.hasFreeIsingLaw_of_root_nonroot_joint line 183