OAI/Geometry/SurfaceImmersion/Correction/UniformGeometricMeanData.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A single geometric mean datum at unit slow scale supplies one fixed profile and actual mean data at all admissible smaller scales.

  1. theorem OAI.ClosedSurfaceR4.PhaseMean.LocalBounds.atScale line 15
  2. theorem OAI.ClosedSurfaceR4.PhaseMean.LocalBounds.atRadius line 32
  3. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.unit_mean_data_uniform_family line 48