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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The time factor in the second-variation bound needed by the velocity detector. This estimate applies in particular to the Euclidean plane.

  1. theorem OAI.ForcedComputation.exp_sub_one_le_mul_exp line 11
  2. theorem OAI.ForcedComputation.second_variation_bound_sharp_mul line 17