OAI/MathematicalPhysics/Heisenberg/RoutedNetworks.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Heisenberg.HullRouting.radial_hull_bounds line 15
2. lemma OAI.Heisenberg.HullRouting.collapse_finite_fibers line 64
3. lemma OAI.Heisenberg.Geometry.walk_support_mem line 76
4. lemma OAI.Heisenberg.HullRouting.collapse_mem_region line 92
5. theorem OAI.Heisenberg.HullRouting.radial_routing line 106
6. lemma OAI.Heisenberg.RoutedFlow.sum_eq_of_zero_off line 159
7. structure OAI.Heisenberg.RoutedFlow.Network line 173
8. def OAI.Heisenberg.RoutedFlow.Network.gradient line 181
9. def OAI.Heisenberg.RoutedFlow.Network.edges line 183
10. lemma OAI.Heisenberg.RoutedFlow.Network.mem_edges line 186
11. lemma OAI.Heisenberg.RoutedFlow.Network.gradient_zero_of_not_mem line 197
12. def OAI.Heisenberg.RoutedFlow.Network.pairing line 204
13. lemma OAI.Heisenberg.RoutedFlow.Network.pairing_eq_sum line 207
14. def OAI.Heisenberg.RoutedFlow.Network.UnitFlow line 217
15. lemma OAI.Heisenberg.RoutedFlow.Network.pairing_finsupp line 219
16. def OAI.Heisenberg.RoutedFlow.pullback line 232
17. lemma OAI.Heisenberg.RoutedFlow.pullback_apply line 239
18. structure OAI.Heisenberg.RoutedFlow.Routing line 242
19. def OAI.Heisenberg.RoutedFlow.Routing.sources line 250
20. lemma OAI.Heisenberg.RoutedFlow.Routing.mem_sources line 252
21. def OAI.Heisenberg.RoutedFlow.Routing.push line 255
22. lemma OAI.Heisenberg.RoutedFlow.Routing.push_eq_sum line 258
23. lemma OAI.Heisenberg.RoutedFlow.Routing.pairing_push line 267
24. lemma OAI.Heisenberg.RoutedFlow.Routing.source_gradient_zero line 286
25. theorem OAI.Heisenberg.RoutedFlow.Routing.push_unit line 298