OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Scalar/PlaneIntegralBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative error bounds used by the compact-test mass argument.

  1. theorem OAI.ForcedComputation.VelocityDetector.abs_increment_le_of_derivative_bound line 11
  2. theorem OAI.ForcedComputation.VelocityDetector.abs_integral_mul_le line 35
  3. theorem OAI.ForcedComputation.VelocityDetector.lower_increment_of_derivative_bound line 52