OAI/MathematicalPhysics/NavierStokes/VelocityDetection/RoutingArrayTrace.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.VelocityDetection.RoutingArray.Trace line 22
  2. def OAI.VelocityDetection.RoutingArray.Trace.sign line 47
  3. def OAI.VelocityDetection.RoutingArray.Trace.Stops line 49
  4. def OAI.VelocityDetection.RoutingArray.point line 51
  5. def OAI.VelocityDetection.RoutingArray.runPath line 54
  6. theorem OAI.VelocityDetection.RoutingArray.contDiff_runPath line 59
  7. theorem OAI.VelocityDetection.RoutingArray.runPath_start line 62
  8. theorem OAI.VelocityDetection.RoutingArray.runPath_end line 66
  9. theorem OAI.VelocityDetection.RoutingArray.runPath_joins line 71
  10. theorem OAI.VelocityDetection.RoutingArray.runPath_eq_installed line 76
  11. theorem OAI.VelocityDetection.RoutingArray.runPath_plateau line 83
  12. theorem OAI.VelocityDetection.RoutingArray.runPath_negative line 90
  13. def OAI.VelocityDetection.RoutingArray.loss line 97
  14. theorem OAI.VelocityDetection.RoutingArray.loss_lt line 100
  15. theorem OAI.VelocityDetection.RoutingArray.loading_loss_le_loss line 103
  16. theorem OAI.VelocityDetection.RoutingArray.retained_loading line 144
  17. theorem OAI.VelocityDetection.RoutingArray.retained_at_loading_end line 181
  18. theorem OAI.VelocityDetection.RoutingArray.retained_stages line 198
  19. theorem OAI.VelocityDetection.RoutingArray.nonterminal_mass_small line 257
  20. theorem OAI.VelocityDetection.RoutingArray.terminal_mass_large line 290
  21. theorem OAI.VelocityDetection.RoutingArray.scalar_detection line 330
  22. theorem OAI.VelocityDetection.RoutingArray.velocity_detection line 362