OAI/MathematicalPhysics/Heisenberg/FlowRouting.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Heisenberg.Flow.lattice_flow_finite_energy line 17
  2. def OAI.Heisenberg.Flow.next line 36
  3. lemma OAI.Heisenberg.Flow.next_down line 38
  4. lemma OAI.Heisenberg.Flow.down_next line 42
  5. lemma OAI.Heisenberg.Flow.next_ne line 46
  6. lemma OAI.Heisenberg.Flow.down_ne line 51
  7. def OAI.Heisenberg.Flow.latticeNetwork line 56
  8. lemma OAI.Heisenberg.Flow.incident_set line 68
  9. lemma OAI.Heisenberg.Flow.incident_disjoint line 82
  10. lemma OAI.Heisenberg.Flow.latticeNetwork_divergence line 94
  11. theorem OAI.Heisenberg.Flow.latticeNetwork_unit line 102
  12. lemma OAI.Heisenberg.Geometry.lattice_neighbor_finite line 112
  13. lemma OAI.Heisenberg.Flow.next_step line 127
  14. lemma OAI.Heisenberg.Flow.down_sub line 133
  15. lemma OAI.Heisenberg.Flow.translated_unit line 138
  16. theorem OAI.Heisenberg.Flow.routed_lattice line 147
  17. lemma OAI.Heisenberg.Flow.radius_eq_norm line 207
  18. lemma OAI.Heisenberg.Flow.lattice_flow_dist_bound line 218
  19. lemma OAI.Heisenberg.Flow.congestion_bound line 222
  20. lemma OAI.Heisenberg.Flow.inverse_power_bound line 235
  21. theorem OAI.Heisenberg.Flow.routed_envelope line 240