MeasuredCoordinateInput.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Measuring the actual coordinate approximations

De Philippis--Gigli (2018), Theorems1.2--1.3, specialize noncollapsed measured convergence to Euclidean metric limits. On balls with Euclidean boundary of zero measure, every measurable metric approximation has the same normalized weak-measure limit. This fixed-radius bounded-Lipschitz form retains the actual coordinate map used by the affine-fit argument.

def OAI.RegularPointCoordinates.LocalMeasuredCoordinateInput line 24
Source documentation
Quantitative Euclidean specialization of noncollapsed measured convergence. The input is metric approximation on a larger ball; the output adds normalized test-integral control on the smaller ball.
```
def LocalMeasuredCoordinateInput {K : ℝ} {n : ℕ} (_hX : NoncollapsedRCD K n X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD