OAI/Geometry/SurfaceImmersion/Correction/ChartedUniformFiniteMean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform threshold for the actual finite family of transported means. The profiles, target and their bounds precede the threshold; the map, both scales, and the actual polynomial solvers follow it.

  1. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.uniform_charted_family_majorants line 15
  2. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.uniform_finite_charted_quadratic_mean line 37