OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/FourShearSchedule.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Four separated rational time slots give an actual smooth planar trajectory for a reciprocal affine map. The global curve is polynomial in the four smooth clocks, so no piecewise path or logarithmic coefficient is needed.

  1. def OAI.ForcedComputation.PlanarHamiltonian.slotStart line 16
  2. def OAI.ForcedComputation.PlanarHamiltonian.slotFinish line 18
  3. theorem OAI.ForcedComputation.PlanarHamiltonian.slot_order line 20
  4. def OAI.ForcedComputation.PlanarHamiltonian.slotClock line 24
  5. def OAI.ForcedComputation.PlanarHamiltonian.slotPulse line 26
  6. theorem OAI.ForcedComputation.PlanarHamiltonian.slotClock_smooth line 28
  7. theorem OAI.ForcedComputation.PlanarHamiltonian.slotClock_hasDerivAt line 31
  8. def OAI.ForcedComputation.PlanarHamiltonian.slotRegion line 35
  9. theorem OAI.ForcedComputation.PlanarHamiltonian.slotRegion_open line 39
  10. theorem OAI.ForcedComputation.PlanarHamiltonian.exists_slotRegion line 43
  11. theorem OAI.ForcedComputation.PlanarHamiltonian.previous_finish_lt line 58
  12. theorem OAI.ForcedComputation.PlanarHamiltonian.lt_future_start line 67
  13. theorem OAI.ForcedComputation.PlanarHamiltonian.clock_previous line 81
  14. theorem OAI.ForcedComputation.PlanarHamiltonian.clock_future line 88
  15. def OAI.ForcedComputation.PlanarHamiltonian.route line 95
  16. theorem OAI.ForcedComputation.PlanarHamiltonian.route_smooth line 101
  17. theorem OAI.ForcedComputation.PlanarHamiltonian.route_eq_stage line 111
  18. theorem OAI.ForcedComputation.PlanarHamiltonian.route_eq_stage_near line 142
  19. def OAI.ForcedComputation.PlanarHamiltonian.scheduledVelocity line 148
  20. theorem OAI.ForcedComputation.PlanarHamiltonian.scheduledVelocity_smooth line 151
  21. theorem OAI.ForcedComputation.PlanarHamiltonian.scheduledVelocity_compactSupport line 160
  22. theorem OAI.ForcedComputation.PlanarHamiltonian.scheduledVelocity_integral_eq_zero line 172
  23. theorem OAI.ForcedComputation.PlanarHamiltonian.scheduledVelocity_one_slot line 195
  24. theorem OAI.ForcedComputation.PlanarHamiltonian.route_hasDerivAt line 207
  25. theorem OAI.ForcedComputation.PlanarHamiltonian.route_initial line 218
  26. theorem OAI.ForcedComputation.PlanarHamiltonian.route_final line 227
  27. theorem OAI.ForcedComputation.PlanarHamiltonian.route_bound line 241