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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Explicit differential inequalities for the integrable tail profile.

  1. theorem OAI.ForcedComputation.VelocityDetector.planeBarrierSquare_abs_coordinate line 12
  2. theorem OAI.ForcedComputation.VelocityDetector.planeTailProfile_laplacian_bound line 21
  3. theorem OAI.ForcedComputation.VelocityDetector.planeTailProfile_advection_bound line 38
  4. theorem OAI.ForcedComputation.VelocityDetector.planeTailProfile_generator_bound line 69