OAI/Probability/FreeIsing/Trees/BroadcastConeLocality.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.RootedBroadcast.ofNoise_congr_cone line 11
2. abbrev OAI.Problem367.RootedBroadcast.DescendantVertex line 47
3. abbrev OAI.Problem367.RootedBroadcast.StrictDescendantVertex line 50
4. def OAI.Problem367.RootedBroadcast.coneNoise line 53
5. theorem OAI.Problem367.RootedBroadcast.measurable_coneNoise line 59
6. theorem OAI.Problem367.RootedBroadcast.ofNoise_coneNoise_at_root line 77
7. def OAI.Problem367.RootedBroadcast.coneFactor line 92
8. theorem OAI.Problem367.RootedBroadcast.measurable_coneFactor line 96
9. theorem OAI.Problem367.RootedBroadcast.factor_cone_representation line 102