OAI/Geometry/RCD/Coordinates/VolumeRigidityMain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Regular-point charts under local volume rigidity

Absolute regular-point volume convergence follows from first-order coordinate maps and their image mass. The local volume rigidity hypothesis is De Philippis--Gigli (2018), Theorem 1.6.

  1. theorem OAI.RegularPointCoordinates.regular_coordinates_of_volume_rigidity line 17