OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/BalancedLoader.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

One compact Hamiltonian translation loads the input point. The source and target belong to a fixed rectangle, hence its whole straight path is inside the cutoff plateau and outside the balanced cube after stretching.

  1. def OAI.ForcedComputation.BalancedLoader.start line 15
  2. def OAI.ForcedComputation.BalancedLoader.rectangle line 16
  3. def OAI.ForcedComputation.BalancedLoader.direction line 17
  4. def OAI.ForcedComputation.BalancedLoader.potential line 19
  5. def OAI.ForcedComputation.BalancedLoader.spatial line 22
  6. def OAI.ForcedComputation.BalancedLoader.clock line 23
  7. def OAI.ForcedComputation.BalancedLoader.pulse line 24
  8. def OAI.ForcedComputation.BalancedLoader.planarVelocity line 25
  9. def OAI.ForcedComputation.BalancedLoader.planarPath line 27
  10. def OAI.ForcedComputation.BalancedLoader.raw line 29
  11. def OAI.ForcedComputation.BalancedLoader.velocity line 30
  12. def OAI.ForcedComputation.BalancedLoader.path line 31
  13. theorem OAI.ForcedComputation.BalancedLoader.spatial_smooth line 33
  14. theorem OAI.ForcedComputation.BalancedLoader.planarVelocity_smooth line 36
  15. theorem OAI.ForcedComputation.BalancedLoader.velocity_smooth line 40
  16. theorem OAI.ForcedComputation.BalancedLoader.planarPath_in_rectangle line 44
  17. theorem OAI.ForcedComputation.BalancedLoader.spatial_on_rectangle line 63
  18. theorem OAI.ForcedComputation.BalancedLoader.planarPath_deriv line 69
  19. theorem OAI.ForcedComputation.BalancedLoader.path_deriv line 79
  20. theorem OAI.ForcedComputation.BalancedLoader.path_before line 88
  21. theorem OAI.ForcedComputation.BalancedLoader.path_after line 94
  22. theorem OAI.ForcedComputation.BalancedLoader.path_safe line 101
  23. theorem OAI.ForcedComputation.BalancedLoader.velocity_before line 114
  24. theorem OAI.ForcedComputation.BalancedLoader.velocity_after line 120
  25. def OAI.ForcedComputation.BalancedLoader.rawSupport line 127
  26. def OAI.ForcedComputation.BalancedLoader.support line 128
  27. theorem OAI.ForcedComputation.BalancedLoader.support_compact line 130
  28. theorem OAI.ForcedComputation.BalancedLoader.spatial_support line 133
  29. theorem OAI.ForcedComputation.BalancedLoader.raw_support line 140
  30. theorem OAI.ForcedComputation.BalancedLoader.velocity_support line 168
  31. theorem OAI.ForcedComputation.BalancedLoader.planarVelocity_divergence line 175
  32. theorem OAI.ForcedComputation.BalancedLoader.raw_divergence line 185
  33. theorem OAI.ForcedComputation.BalancedLoader.velocity_divergence line 194