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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The concentration test is constant wherever a moving gate can fail to be a rigid translation. This gives exact transport cancellation.

  1. theorem OAI.ForcedComputation.ExpandingDetector.concentrationCutoff_joint_smooth line 14
  2. theorem OAI.ForcedComputation.ExpandingDetector.concentrationCutoff_fderiv_zero line 22
  3. theorem OAI.ForcedComputation.ExpandingDetector.concentrationCutoff_transport_cancel line 34
  4. def OAI.ForcedComputation.ExpandingDetector.concentrationDerivative line 48
  5. theorem OAI.ForcedComputation.ExpandingDetector.concentrationDerivative_smooth line 51
  6. theorem OAI.ForcedComputation.ExpandingDetector.concentrationDerivative_support line 59