OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/EuclideanReverseVariations.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.euclidean_second_fderiv_fun_neg line 12
  2. theorem OAI.ForcedComputation.EuclideanVariations.reverse line 20
  3. theorem OAI.ForcedComputation.euclidean_first_variation_reverse line 37
  4. theorem OAI.ForcedComputation.euclidean_second_variation_reverse line 46
  5. theorem OAI.ForcedComputation.euclidean_inverse_estimates line 64