OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/MixedOrdering.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Ordered directional derivatives can be grouped into time derivatives and spatial derivatives, by the symmetry already proved for the flat calculus.

  1. theorem OAI.ForcedComputation.mixedDerivative_perm line 14
  2. theorem OAI.ForcedComputation.time_spatial_normal_form line 22
  3. theorem OAI.ForcedComputation.mixedDerivative_time_spatial line 38