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

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Translation to an arbitrary detector center. These identities preserve the actual transition map and both variational equations.

  1. def OAI.ForcedComputation.VelocityDetector.CompactCenter.translateField line 13
  2. def OAI.ForcedComputation.VelocityDetector.CompactCenter.translateTransition line 16
  3. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.translated_smooth line 19
  4. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.translated_periodic line 24
  5. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.translated_fderiv line 30
  6. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.translated_second line 35
  7. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.translated_divergence line 43
  8. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.transition_fderiv line 52
  9. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.transition_second line 58
  10. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.transition_translated line 66
  11. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.variations_translated line 82
  12. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.backward_translated line 99