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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded comparison on the whole plane, proved with an explicit quadratic barrier. No periodicity, decay, integrability or compact support of the scalar is assumed in this argument.

  1. theorem OAI.ForcedComputation.VelocityDetector.scalar_maximum_principle_bounded line 15