MeasuredApproximation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Measured Euclidean approximation and the initial harmonic input

The bounded Lipschitz tests below retain the measure information required by Huang--Huang Theorem 2.9(1); metric GH closeness alone is not substituted for it. The convergence input is the noncollapsed volume/measure convergence of De Philippis--Gigli (2018), Theorems 1.2--1.3.

structure OAI.RegularPointCoordinates.IsMeasuredEuclideanApproximation line 26
Source documentation
A pointed metric approximation together with the normalized measure comparison, tested against all bounded 1-Lipschitz functions.
```
structure IsMeasuredEuclideanApproximation (μ : Measure X) (n : ℕ)
    (p : X) (r R ε : ℝ) (f : X → Euclidean n) : Prop where
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean
def OAI.RegularPointCoordinates.EuclideanMeasuredRescalingConvergence line 37
Source documentation
The Euclidean-limit specialization of noncollapsed measured volume convergence, including approximation maps and normalized test integrals.
```
def EuclideanMeasuredRescalingConvergence (μ : Measure X) (n : ℕ) (p : X) : Prop :=
…
```
theorem OAI.RegularPointCoordinates.regular_small_scale_measured_approximation line 46
Source documentation
All-tangents regularity and the published measured convergence give a uniform scale threshold for measured, not only metric, approximation.
```
theorem regular_small_scale_measured_approximation {μ : Measure X} {n : ℕ} {p : X}
    (hcompact : PointedRescalingPrecompactness p) (hregular : IsRegular n p)
    (hmeasured : EuclideanMeasuredRescalingConvergence μ n p)
    {R ε : ℝ} (hR : 0 < R) (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ r : ℝ, 0 < r → r < δ →
      ∃ f : X → Euclidean n, IsMeasuredEuclideanApproximation μ n p r R ε f := by
…
```
Mentions: OAI.RegularPointCoordinates.PointedRescalingPrecompactness, OAI.RegularPointCoordinates.IsRegular, OAI.RegularPointCoordinates.EuclideanMeasuredRescalingConvergence, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsMeasuredEuclideanApproximation
def OAI.RegularPointCoordinates.LocalInitialSplittingInput line 68
Source documentation
Huang--Huang Theorem 2.9(1), specialized to the Euclidean target. The enlarged measured ball leaves room for a compact Sobolev extension of the local harmonic map without changing it on the output ball.
```
def LocalInitialSplittingInput {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD