OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartTrace.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VelocityDetection.ChartTrace.height line 13
  2. def OAI.VelocityDetection.ChartTrace.vertex line 15
  3. def OAI.VelocityDetection.ChartTrace.segment line 18
  4. theorem OAI.VelocityDetection.ChartTrace.contDiff_segment line 23
  5. theorem OAI.VelocityDetection.ChartTrace.segment_source_collar line 27
  6. theorem OAI.VelocityDetection.ChartTrace.segment_target_collar line 44
  7. theorem OAI.VelocityDetection.ChartTrace.segment_before line 56
  8. theorem OAI.VelocityDetection.ChartTrace.segment_after line 60
  9. theorem OAI.VelocityDetection.ChartTrace.velocity_before line 64
  10. theorem OAI.VelocityDetection.ChartTrace.velocity_after line 73
  11. def OAI.VelocityDetection.ChartTrace.route line 82
  12. theorem OAI.VelocityDetection.ChartTrace.contDiff_route line 85
  13. theorem OAI.VelocityDetection.ChartTrace.route_before line 89
  14. theorem OAI.VelocityDetection.ChartTrace.route_after line 96
  15. theorem OAI.VelocityDetection.ChartTrace.route_eq_segment line 107
  16. theorem OAI.VelocityDetection.ChartTrace.deriv_route line 127
  17. theorem OAI.VelocityDetection.ChartTrace.route_velocity_before line 136
  18. theorem OAI.VelocityDetection.ChartTrace.route_velocity_after line 140
  19. theorem OAI.VelocityDetection.ChartTrace.route_velocity line 148
  20. theorem OAI.VelocityDetection.ChartTrace.segment_eq_installed line 162
  21. theorem OAI.VelocityDetection.ChartTrace.route_plateau line 172