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

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A finite expression for the normalized compact source. Its integral is already proved to be one; evaluation uses only the explicit pulse.

  1. def OAI.ForcedComputation.ExpandingDetector.pulseCode line 13
  2. theorem OAI.ForcedComputation.ExpandingDetector.pulseCode_val line 16
  3. def OAI.ForcedComputation.ExpandingDetector.impulseAxisCode line 22
  4. theorem OAI.ForcedComputation.ExpandingDetector.impulseAxisCode_val line 25
  5. def OAI.ForcedComputation.ExpandingDetector.unitImpulseCode line 37
  6. theorem OAI.ForcedComputation.ExpandingDetector.unitImpulseCode_val line 40
  7. def OAI.ForcedComputation.ExpandingDetector.verticalSourceCode line 46
  8. theorem OAI.ForcedComputation.ExpandingDetector.verticalSourceCode_val line 49