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

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The same variational input controls reverse transitions. No separate regularity hypothesis for an inverse map is needed.

  1. theorem OAI.ForcedComputation.second_fderiv_fun_neg line 12
  2. theorem OAI.ForcedComputation.PlanarVariations.reverse line 20
  3. theorem OAI.ForcedComputation.planar_first_variation_reverse line 37
  4. theorem OAI.ForcedComputation.planar_second_variation_reverse line 46
  5. theorem OAI.ForcedComputation.planar_inverse_estimates line 64