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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The first and second variational equations follow by differentiating the actual ODE after joint smoothness has been proved.

  1. theorem OAI.ForcedComputation.Flow.first_variation line 14
  2. theorem OAI.ForcedComputation.Flow.second_variation line 37