OAI/Probability/FreeIsing/Trees/BroadcastLocality.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem367.RootedBroadcast.ofNoise_congr_prefix line 10
2. lemma OAI.Problem367.RootedBroadcast.factor_congr_prefix line 37
3. abbrev OAI.Problem367.RootedBroadcast.BranchVertex line 44
4. lemma OAI.Problem367.RootedBroadcast.prefix_in_branch_or_root line 46
5. def OAI.Problem367.RootedBroadcast.branchNoise line 56
6. lemma OAI.Problem367.RootedBroadcast.measurable_branchNoise line 62
7. def OAI.Problem367.RootedBroadcast.branchFactor line 76
8. lemma OAI.Problem367.RootedBroadcast.measurable_branchFactor line 80
9. lemma OAI.Problem367.RootedBroadcast.factor_branch_representation line 86