OAI/Geometry/RCD/Harmonic/AffineImprovementTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Affine improvement in the original harmonic coordinate span

The measured compactness theorem is applied to normalized and recentered coordinates. Invertibility and the local constant cutoff identify their affine projection exactly with that of the original columns.

  1. theorem OAI.RegularPointCoordinates.affine_improvement_from_metric_coordinates line 23