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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite-time velocity and gradient bounds required by the whole-plane comparison class. Compact support is needed only for the prescribed drift.

  1. theorem OAI.ForcedComputation.VelocityDetector.CompactPlaneCoefficients.drift_derivative_bound line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.triangularLift_norm_bound line 35
  3. theorem OAI.ForcedComputation.VelocityDetector.triangularLift_fderiv_norm_bound line 48
  4. theorem OAI.ForcedComputation.VelocityDetector.PlaneScalarSolution.velocity_gradient_bound line 76