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

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The nonnegative height-one periodic bump injected by a detector block. Its center is the fixed planar processor point (1/4,1/4).

  1. def OAI.ForcedComputation.VelocityDetector.detectorProfile line 13
  2. def OAI.ForcedComputation.VelocityDetector.detectorBump line 16
  3. theorem OAI.ForcedComputation.VelocityDetector.detectorProfile_smooth line 19
  4. theorem OAI.ForcedComputation.VelocityDetector.detectorProfile_periodic line 23
  5. theorem OAI.ForcedComputation.VelocityDetector.detectorProfile_in_chart line 26
  6. theorem OAI.ForcedComputation.VelocityDetector.detectorProfile_range line 33
  7. theorem OAI.ForcedComputation.VelocityDetector.detectorProfile_center line 41
  8. theorem OAI.ForcedComputation.VelocityDetector.detectorBump_smooth line 46
  9. theorem OAI.ForcedComputation.VelocityDetector.detectorBump_periodic line 51
  10. theorem OAI.ForcedComputation.VelocityDetector.detectorBump_range line 57
  11. theorem OAI.ForcedComputation.VelocityDetector.detectorBump_center line 63
  12. theorem OAI.ForcedComputation.VelocityDetector.detectorBump_support_in_chart line 68