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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A moving compact test loses at most the diffusion budget. Transport cancellation is an identity of the concrete test and velocity, while scalar positivity and total mass are supplied by the preceding PDE lemmas.

  1. theorem OAI.ForcedComputation.VelocityDetector.PlaneScalarSolution.moving_mass_derivative_lower line 16