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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Positive derivatives of the gate centers. The constant starting position disappears, so the estimate retains the reciprocal time scale.

  1. theorem OAI.ForcedComputation.ExpandingDetector.weight_derivative_bounds line 13
  2. theorem OAI.ForcedComputation.ExpandingDetector.affine_clock_derivative_bound line 30
  3. theorem OAI.ForcedComputation.ExpandingDetector.scheduledCenter_horizontal_jet line 55
  4. theorem OAI.ForcedComputation.ExpandingDetector.scheduledCenter_vertical_jet line 70