OAI/Geometry/SurfaceImmersion/Correction/WeightedPolynomialVariation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A first-variation estimate for every finite higher-jet polynomial. Its scale exponent is fixed by the polynomial, independently of output order.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.weighted_plain_jet line 14
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_ge_two line 32
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.increase_loss line 38
  4. theorem OAI.ClosedSurfaceR4.JetPolynomial.Expression.compact_variation_bound line 44