OAI/Geometry/RCD/Coordinates/RegularControlledNormalization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Harmonic normalization around a regular point

Initial harmonic approximation, all-center metric flatness, a finite-dimensional obstruction, and the transformation theorem produce normalized harmonic coordinates.

  1. theorem OAI.RegularPointCoordinates.regular_controlled_normalization line 23