OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/ExpandingGateMotion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Joint smoothness of the moving Hamiltonian translation gates, including their motion through the cutoff collars.

  1. theorem OAI.ForcedComputation.ExpandingDetector.timeHamiltonianField_smooth line 15
  2. theorem OAI.ForcedComputation.ExpandingDetector.translationGate_zero_velocity line 22
  3. def OAI.ForcedComputation.ExpandingDetector.movingGate line 27
  4. theorem OAI.ForcedComputation.ExpandingDetector.movingGate_smooth line 30
  5. theorem OAI.ForcedComputation.ExpandingDetector.movingGate_zero_of_constant_near line 46
  6. theorem OAI.ForcedComputation.ExpandingDetector.movingGate_tracks line 51