OAI/Geometry/SurfaceImmersion/Correction/UniformGeometricAtlasMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Global charted mean data constructed from fixed unit-scale geometry. The global trial radius is selected after the atlas amplification bound.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.uniform_geometric_atlas_mean line 31