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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A fixed compact cutoff, rescaled to each expanding gate. Its exact plateau has radius twice the gate radius, with support of radius three.

  1. def OAI.ForcedComputation.ExpandingDetector.unitGateBox line 14
  2. def OAI.ForcedComputation.ExpandingDetector.gateCutoff line 16
  3. theorem OAI.ForcedComputation.ExpandingDetector.gateCutoff_eq_profiles line 19
  4. theorem OAI.ForcedComputation.ExpandingDetector.gateCutoff_smooth line 24
  5. theorem OAI.ForcedComputation.ExpandingDetector.gateCutoff_range line 30
  6. theorem OAI.ForcedComputation.ExpandingDetector.gateCutoff_one_near line 43
  7. theorem OAI.ForcedComputation.ExpandingDetector.gateCutoff_support line 68
  8. theorem OAI.ForcedComputation.ExpandingDetector.gateCutoff_tsupport line 82
  9. theorem OAI.ForcedComputation.ExpandingDetector.gateCutoff_compactSupport line 92