OAI/Geometry/SurfaceImmersion/Correction/RealPolynomialVariationBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounds for arbitrary real variations at the short scale. These are the nonoscillatory estimates used for mixed terms and the Taylor remainder.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.realVariation line 13
  2. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.compact_real_variation_bound line 17