VolumeRigidityInput.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The published half-ball volume-rigidity input

De Philippis--Gigli (2018), Theorem 1.6, gives GH control of the half ball. We retain that radius loss and use an unpointed ball approximation. The centering and fixed metric-rescaling steps are proved in Lean.

def OAI.RegularPointCoordinates.euclideanUnitVolume line 20
theorem OAI.RegularPointCoordinates.euclideanUnitVolume_pos line 23
def OAI.RegularPointCoordinates.LocalVolumeRigidityInput line 31
Source documentation
The map formulation of De Philippis--Gigli Theorem 1.6. The universal error absorbs the usual factor between GH distance and approximation maps.
```
def LocalVolumeRigidityInput {K : ℝ} {n : ℕ} (_hX : NoncollapsedRCD K n X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD
theorem OAI.RegularPointCoordinates.pointed_flatness_of_volume_rigidity line 39
Source documentation
Nearly maximal volume on B_(4r) yields a pointed Euclidean approximation on B_(2r), with the prescribed normalized error.
```
theorem pointed_flatness_of_volume_rigidity {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) (hpublished : LocalVolumeRigidityInput hX)
    {θ : ℝ} (hθ : 0 < θ) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ (p : X) (r : ℝ), 0 < r → -δ ≤ K * (4 * r) ^ 2 →
      (1 - δ) * euclideanUnitVolume n * (4 * r) ^ n ≤
        (hausdorff n X).real (ball p (4 * r)) →
      ∃ f : X → Euclidean n, IsPointedApproximation p 0 r 2 θ f := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalVolumeRigidityInput, OAI.RegularPointCoordinates.euclideanUnitVolume, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation