OAI/Geometry/SurfaceImmersion/Correction/PolynomialTaylorRemainder.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The weighted cubic estimate for the actual higher-jet polynomial map.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.affinePolynomial_apply line 12
  2. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.taylorRemainder line 17
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.cubicRemainder_affine line 21
  4. theorem OAI.ClosedSurfaceR4.JetPolynomial.Expression.taylorRemainder_eq_integral line 31
  5. theorem OAI.ClosedSurfaceR4.JetPolynomial.Expression.weighted_taylorRemainder line 40