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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Discharge of the smooth-dependence and variational-equation input for the actual finite-expression planar transition. All analytic ingredients are proved from the library implicit-function theorem and ODE uniqueness.

  1. theorem OAI.ForcedComputation.variations_of_joint_smooth line 15
  2. theorem OAI.ForcedComputation.planarTransition_variations line 32
  3. theorem OAI.ForcedComputation.exists_planarTransition_with_variations line 39