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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Derivative bounds for one moving gate, expressed through the velocity and the rescaled center. Only positive derivatives of the center enter.

  1. def OAI.ForcedComputation.ExpandingDetector.gatePacket line 14
  2. theorem OAI.ForcedComputation.ExpandingDetector.gatePacket_jet_bound line 17