OAI/MathematicalPhysics/Heisenberg/LatticeFlows.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Heisenberg.Flow.Orthant line 18
  2. def OAI.Heisenberg.Flow.level line 20
  3. def OAI.Heisenberg.Flow.layerMass line 22
  4. lemma OAI.Heisenberg.Flow.layerMass_pos line 24
  5. lemma OAI.Heisenberg.Flow.layerMass_zero line 28
  6. lemma OAI.Heisenberg.Flow.layerMass_recurrence line 30
  7. def OAI.Heisenberg.Flow.orthantFlow line 46
  8. lemma OAI.Heisenberg.Flow.flow_nonneg line 49
  9. lemma OAI.Heisenberg.Flow.coord_le_level line 54
  10. lemma OAI.Heisenberg.Flow.outgoing line 57
  11. def OAI.Heisenberg.Flow.predecessor line 65
  12. lemma OAI.Heisenberg.Flow.predecessor_level line 68
  13. lemma OAI.Heisenberg.Flow.level_zero_iff line 83
  14. lemma OAI.Heisenberg.Flow.incoming line 92
  15. theorem OAI.Heisenberg.Flow.orthant_divergence line 116
  16. lemma OAI.Heisenberg.Flow.flow_le_layerMass line 125
  17. lemma OAI.Heisenberg.Flow.layerMass_decay line 134
  18. theorem OAI.Heisenberg.Flow.orthant_flow_envelope line 146
  19. abbrev OAI.Heisenberg.Flow.ZSite line 155
  20. def OAI.Heisenberg.Flow.PositiveOrthant line 157
  21. def OAI.Heisenberg.Flow.natPart line 159
  22. def OAI.Heisenberg.Flow.down line 161
  23. def OAI.Heisenberg.Flow.latticeFlow line 164
  24. lemma OAI.Heisenberg.Flow.down_positive line 167
  25. lemma OAI.Heisenberg.Flow.positive_of_down line 179
  26. lemma OAI.Heisenberg.Flow.natPart_down line 190
  27. lemma OAI.Heisenberg.Flow.natPart_zero_iff line 199
  28. lemma OAI.Heisenberg.Flow.lattice_incoming_formula line 210
  29. theorem OAI.Heisenberg.Flow.lattice_divergence line 221
  30. def OAI.Heisenberg.Flow.radius line 236
  31. lemma OAI.Heisenberg.Flow.radius_le_level line 238
  32. theorem OAI.Heisenberg.Flow.lattice_flow_envelope line 249