OAI/MathematicalPhysics/AlternatingFlow/Construction.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AlternatingNS.Construction.donorIndex line 12
  2. def OAI.AlternatingNS.Construction.receiverIndex line 16
  3. lemma OAI.AlternatingNS.Construction.indices_distinct line 20
  4. def OAI.AlternatingNS.Construction.slot line 25
  5. def OAI.AlternatingNS.Construction.loading line 30
  6. def OAI.AlternatingNS.Construction.piece line 36
  7. def OAI.AlternatingNS.Construction.velocity line 39
  8. lemma OAI.AlternatingNS.Construction.slot_smooth line 42
  9. lemma OAI.AlternatingNS.Construction.loading_smooth line 45
  10. lemma OAI.AlternatingNS.Construction.piece_smooth line 48
  11. lemma OAI.AlternatingNS.Construction.piece_support line 53
  12. lemma OAI.AlternatingNS.Construction.piece_div line 57
  13. lemma OAI.AlternatingNS.Construction.velocity_smooth line 65
  14. lemma OAI.AlternatingNS.Construction.velocity_supported line 70
  15. lemma OAI.AlternatingNS.Construction.velocity_rest line 79
  16. lemma OAI.AlternatingNS.Construction.velocity_div line 83
  17. lemma OAI.AlternatingNS.Construction.slot_plateau line 98
  18. lemma OAI.AlternatingNS.Construction.loading_plateau line 104
  19. lemma OAI.AlternatingNS.Construction.donorIndex_succ line 116
  20. lemma OAI.AlternatingNS.Construction.donorIndex_eq line 120
  21. def OAI.AlternatingNS.Construction.memory line 124
  22. def OAI.AlternatingNS.Construction.history line 128
  23. def OAI.AlternatingNS.Construction.displacement line 131
  24. def OAI.AlternatingNS.Construction.node line 138
  25. def OAI.AlternatingNS.Construction.path line 142
  26. lemma OAI.AlternatingNS.Construction.memory_zero_coord line 145
  27. lemma OAI.AlternatingNS.Construction.memory_donor line 149
  28. lemma OAI.AlternatingNS.Construction.memory_succ line 156
  29. lemma OAI.AlternatingNS.Construction.history_zero_coord line 161
  30. lemma OAI.AlternatingNS.Construction.history_donor line 165
  31. lemma OAI.AlternatingNS.Construction.history_succ line 169
  32. lemma OAI.AlternatingNS.Construction.observedParticle_eq line 174
  33. lemma OAI.AlternatingNS.Construction.node_succ line 179
  34. lemma OAI.AlternatingNS.Construction.node_sum line 188
  35. lemma OAI.AlternatingNS.Construction.path_slot line 194
  36. lemma OAI.AlternatingNS.Construction.path_node line 199
  37. lemma OAI.AlternatingNS.Construction.memory_bound line 203
  38. lemma OAI.AlternatingNS.Construction.node_plateau line 229
  39. lemma OAI.AlternatingNS.Construction.segment_plateau line 249
  40. lemma OAI.AlternatingNS.Construction.path_plateau line 261
  41. lemma OAI.AlternatingNS.Construction.path_donor line 280
  42. lemma OAI.AlternatingNS.Construction.piece_path line 290
  43. lemma OAI.AlternatingNS.Construction.velocity_path line 304
  44. theorem OAI.AlternatingNS.Construction.path_isTrajectory line 313
  45. lemma OAI.AlternatingNS.Construction.path_loading_coord line 323
  46. lemma OAI.AlternatingNS.Construction.path_slot_coord line 329
  47. theorem OAI.AlternatingNS.Construction.path_reachability line 337