OAI/Geometry/SurfaceImmersion/Correction/PolynomialQuadraticTensorBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The three tensor components use a common derivative order and a common short-scale exponent, independently of the number of correction steps.

  1. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.quadraticFamilyTensor_bound line 13