HarmonicMomentCompactnessInput.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The local harmonic-compactness input, restricted to finite moments

Ambrosio--Honda (2018), Local spectral convergence in RCD*(K,N) spaces, Theorem 4.2, Theorem 4.4 and Corollary 4.5, specialized to a Euclidean measured limit. Strong local L² convergence implies convergence of the pairings with constants and the bounded coordinate functions. The hypothesis below retains the local rescaled H¹ bound needed by those theorems. It asserts neither an affine approximation nor a chart.

def OAI.RegularPointCoordinates.LocalHarmonicMomentCompactnessInput line 27
Source documentation
Only the normalized moments of one harmonic function and the finite coordinate family are retained from the published local compactness theorem. All target functions are genuine Sobolev functions of the original space.
```
def LocalHarmonicMomentCompactnessInput {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD