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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Positivity and comparison from the whole-plane maximum principle.

  1. theorem OAI.ForcedComputation.VelocityDetector.CompactPlaneCoefficients.drift_bound line 12
  2. theorem OAI.ForcedComputation.VelocityDetector.CompactPlaneCoefficients.sub line 27
  3. theorem OAI.ForcedComputation.VelocityDetector.PlaneScalarSolution.nonnegative line 42
  4. theorem OAI.ForcedComputation.VelocityDetector.PlaneScalarSolution.sub line 64
  5. theorem OAI.ForcedComputation.VelocityDetector.PlaneScalarSolution.compare line 87
  6. theorem OAI.ForcedComputation.VelocityDetector.PlaneScalarSolution.unique line 98