OAI/Probability/FreeIsing/Trees/BroadcastOutsideCone.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem367.RootedBroadcast.OutsideConeVertex line 11
2. abbrev OAI.Problem367.RootedBroadcast.OutsideConeNonroot line 14
3. def OAI.Problem367.RootedBroadcast.outsideConeNoise line 17
4. theorem OAI.Problem367.RootedBroadcast.measurable_outsideConeNoise line 22
5. theorem OAI.Problem367.RootedBroadcast.outsideConeNoise_ofNoise_eq_rootless line 33
6. def OAI.Problem367.RootedBroadcast.outsideConeFactor line 46
7. theorem OAI.Problem367.RootedBroadcast.measurable_outsideConeFactor line 53
8. theorem OAI.Problem367.RootedBroadcast.factor_outsideCone_representation line 69