OAI/Geometry/SurfaceImmersion/Correction/UniformPerturbedMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite perturbed mean construction with its threshold fixed before the slow scale and the target tensor. This ordering is needed when both vary at successive stages of the primitive realization.

  1. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.uniform_perturbed_mean line 15