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

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The scalar source installs every test block without simulating the machine. Its locally finite sum is smooth, periodic, and nonnegative.

  1. theorem OAI.ForcedComputation.VelocityDetector.detector_width_small line 15
  2. def OAI.ForcedComputation.VelocityDetector.detectorSourceTerm line 24
  3. def OAI.ForcedComputation.VelocityDetector.detectorSource line 29
  4. theorem OAI.ForcedComputation.VelocityDetector.detectorSourceTerm_smooth line 32
  5. theorem OAI.ForcedComputation.VelocityDetector.detectorSourceTerm_before line 39
  6. theorem OAI.ForcedComputation.VelocityDetector.detectorSourceTerm_nonnegative line 47
  7. theorem OAI.ForcedComputation.VelocityDetector.detectorSource_smooth line 55
  8. theorem OAI.ForcedComputation.VelocityDetector.detectorSource_nonnegative line 59
  9. theorem OAI.ForcedComputation.VelocityDetector.detectorSource_periodic line 63
  10. theorem OAI.ForcedComputation.VelocityDetector.detectorSource_before line 70
  11. theorem OAI.ForcedComputation.VelocityDetector.detectorSource_before_one line 83