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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact tests depending on time. This is the local transport identity used to retain scalar mass inside each moving computation gate.

  1. theorem OAI.ForcedComputation.VelocityDetector.PlaneScalarSolution.moving_test_derivative line 13