OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/CylinderEnergyEquation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Subtraction of the two classical Navier–Stokes equations, in the ordering used by the localized difference-energy identity.

  1. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.gradient_sub line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.advection_difference line 22
  3. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.cylinder_difference_equation line 30