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

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Translation of the prescribed full force. The coordinate formulas also give a finite evaluator for every effective center, by translating the input oracle and the evaluation point in opposite directions.

  1. def OAI.ForcedComputation.VelocityDetector.CompactCenter.shiftVector line 16
  2. def OAI.ForcedComputation.VelocityDetector.CompactCenter.shiftSpaceTime line 17
  3. def OAI.ForcedComputation.VelocityDetector.CompactCenter.translateVelocity line 18
  4. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.horizontal_shift line 21
  5. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.components_translated line 26
  6. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.mixedDerivative_translated line 35
  7. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.vectorLaplacian_translated line 48
  8. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.planarResidual_translated line 62
  9. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.triangularForce_translated line 74
  10. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.centeredForce_translated line 82
  11. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.centeredForce_mixed line 98
  12. def OAI.ForcedComputation.VelocityDetector.CompactCenter.negatePoint line 104
  13. def OAI.ForcedComputation.VelocityDetector.CompactCenter.negateName line 105
  14. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.rationalPoint_negate line 107
  15. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.negateName_spec line 113
  16. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.shiftSpaceTime_neg line 119
  17. def OAI.ForcedComputation.VelocityDetector.CompactCenter.translatedInputOracle line 125
  18. def OAI.ForcedComputation.VelocityDetector.CompactCenter.evaluateCenteredForce line 132
  19. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.evaluateCenteredForce_spec line 141
  20. def OAI.ForcedComputation.VelocityDetector.CompactCenter.centeredForceBound line 156
  21. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.centeredForceBound_spec line 162