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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds for every time derivative of the gate velocity retain one reciprocal duration factor, including the zeroth velocity derivative.

  1. theorem OAI.ForcedComputation.ExpandingDetector.deriv_component line 13
  2. theorem OAI.ForcedComputation.ExpandingDetector.iteratedDeriv_velocity_component line 19
  3. theorem OAI.ForcedComputation.ExpandingDetector.scheduledVelocity_joint_jet line 27