OAI/MathematicalPhysics/Heisenberg/NetworkEnergy.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Heisenberg.RoutedFlow.Network.boundary line 15
2. def OAI.Heisenberg.RoutedFlow.Network.divergence line 18
3. lemma OAI.Heisenberg.RoutedFlow.Network.vertex_sum line 21
4. lemma OAI.Heisenberg.RoutedFlow.Network.boundary_zero line 31
5. lemma OAI.Heisenberg.RoutedFlow.Network.divergence_eq_sum line 36
6. theorem OAI.Heisenberg.RoutedFlow.Network.pairing_divergence line 46
7. theorem OAI.Heisenberg.RoutedFlow.Network.unit_of_divergence line 59
8. lemma OAI.Heisenberg.RoutedFlow.Network.pairing_single line 69
9. lemma OAI.Heisenberg.RoutedFlow.Network.pairing_add line 74
10. theorem OAI.Heisenberg.RoutedFlow.Routing.abs_push_le line 83
11. def OAI.Heisenberg.RoutedFlow.graphNetwork line 103
12. def OAI.Heisenberg.RoutedFlow.pathCurrent line 119
13. lemma OAI.Heisenberg.RoutedFlow.pathCurrent_pairing line 123
14. lemma OAI.Heisenberg.RoutedFlow.pathCurrent_eq_count line 133
15. lemma OAI.Heisenberg.RoutedFlow.pathCurrent_abs_le_one line 145
16. lemma OAI.Heisenberg.RoutedFlow.pathCurrent_ne_zero_iff line 152
17. def OAI.Heisenberg.RoutedFlow.routingOfPaths line 156
18. lemma OAI.Heisenberg.RoutedFlow.routingOfPaths_abs_le_one line 163
19. abbrev OAI.Heisenberg.LatticeSum.Site line 175
20. def OAI.Heisenberg.LatticeSum.radius line 177
21. def OAI.Heisenberg.LatticeSum.integerLattice line 179
22. instance OAI.Heisenberg.LatticeSum.(instance at line 182) line 182
23. instance OAI.Heisenberg.LatticeSum.(instance at line 186) line 186
24. def OAI.Heisenberg.LatticeSum.embed line 190
25. lemma OAI.Heisenberg.LatticeSum.embed_injective line 196
26. lemma OAI.Heisenberg.LatticeSum.embed_norm_le line 203
27. lemma OAI.Heisenberg.LatticeSum.embed_ne_zero line 212
28. theorem OAI.Heisenberg.LatticeSum.summable_radius_rpow line 221
29. theorem OAI.Heisenberg.LatticeSum.summable_radius_sub_rpow line 239
30. theorem OAI.Heisenberg.LatticeSum.finite_energy_of_envelope line 243