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

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact isolation of each burst and the following heat-only waiting interval. The endpoints are included because the smooth pulses vanish there.

  1. theorem OAI.ForcedComputation.VelocityDetector.detectorSourceTerm_before_closed line 12
  2. theorem OAI.ForcedComputation.VelocityDetector.detectorDriftTerm_before_closed line 20
  3. theorem OAI.ForcedComputation.VelocityDetector.detectorDriftTerm_after line 26
  4. theorem OAI.ForcedComputation.VelocityDetector.detector_duration_real_le line 32
  5. theorem OAI.ForcedComputation.VelocityDetector.detector_other_block_inactive line 37
  6. theorem OAI.ForcedComputation.VelocityDetector.detectorDrift_eq_term line 50
  7. theorem OAI.ForcedComputation.VelocityDetector.detectorSource_eq_term line 60
  8. theorem OAI.ForcedComputation.VelocityDetector.detector_wait_coefficients_zero line 71