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

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Rational translation of the finite pulse data. The cutoff support and its positive separation are translated together. Local field covariance is all that is needed by the tracked paths.

  1. def OAI.ForcedComputation.PlanarRouting.translatedPoint line 15
  2. def OAI.ForcedComputation.PlanarRouting.translatedBox line 17
  3. theorem OAI.ForcedComputation.PlanarRouting.translatedBox_positive line 20
  4. theorem OAI.ForcedComputation.PlanarRouting.mem_translatedBox line 26
  5. theorem OAI.ForcedComputation.PlanarRouting.translatedBox_gap line 31
  6. def OAI.ForcedComputation.PlanarHamiltonian.Primitive.translated line 47
  7. theorem OAI.ForcedComputation.PlanarHamiltonian.Primitive.translated_field line 51
  8. def OAI.ForcedComputation.PlanarHamiltonian.Pulse.translated line 67
  9. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.translated_valid line 74
  10. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.spatial_on_rectangle line 77
  11. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.translated_spatial line 81
  12. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.translated_velocity line 88
  13. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.translated_inUnit line 95
  14. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.translated_hasDerivAt line 108