OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/FlowMixedPartials.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Commutation of a time derivative and an initial-point derivative. These lemmas turn joint smoothness of an actual flow into its variational equations, without an additional smooth-dependence input.

  1. theorem OAI.ForcedComputation.Flow.spaceDerivative_eq line 19
  2. theorem OAI.ForcedComputation.Flow.timeDerivative_eq line 26
  3. theorem OAI.ForcedComputation.Flow.spaceDerivative_smooth line 32
  4. theorem OAI.ForcedComputation.Flow.time_space_commute line 41