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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The quantitative inequalities needed for the first two variational equations of the planar processor. Doubling the computed coefficient bound puts both estimates in the form used in the manuscript.

  1. theorem OAI.ForcedComputation.first_variation_bound_mul line 15
  2. theorem OAI.ForcedComputation.first_variation_bound line 25
  3. theorem OAI.ForcedComputation.second_variation_bound_mul line 32
  4. theorem OAI.ForcedComputation.second_variation_bound line 67