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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The mass identity at every nonnegative time of a smooth global scalar solution. Only the equation at that time is needed.

  1. def OAI.ForcedComputation.VelocityDetector.scalarTimeDerivative line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.scalarTimeDerivative_smooth line 17
  3. theorem OAI.ForcedComputation.VelocityDetector.scalarTimeDerivative_hasDerivAt line 22
  4. theorem OAI.ForcedComputation.VelocityDetector.GlobalTorusScalarSolution.mass_hasDerivAt line 28