OAI/Geometry/SurfaceImmersion/Correction/NormalizedPolynomialMean.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The polynomial part of the normalized quadratic mean is O(η), with finite-loss value and difference bounds and constants chosen before scales.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.normalizedPolynomialMean line 13
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.normalized_product_scale line 17
  3. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.normalizedPolynomialMean_bounds line 38