PoissonHarmonicCompactnessInput.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

local compactness including radial gradient pairings

Ambrosio--Honda, Local spectral convergence in RCD(K,N) spaces* (2018), Theorems 4.2, 4.4 and 4.6(2), Corollaries 4.3 and 4.5. This specialization retains one harmonic function and one bounded-Laplacian function converging in value to the squared Euclidean radius. The local gradient bound for the latter and the harmonic energy bound give the L2 bound required in 4.6(2). The conclusion records weak test pairings and finite value moments only.

def OAI.RegularPointCoordinates.InteriorSmoothTest line 22
structure OAI.RegularPointCoordinates.PoissonHarmonicLimit line 29
Source documentation
Precisely the weak pairings retained from the local strong/weak Sobolev convergence theorem, with the physical radius factors explicit.
```
structure PoissonHarmonicLimit {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X)
    (S : ℝ) (p : ℕ → X) (r : ℕ → ℝ)
    (u : ℕ → Fin n → SobolevSpace (hausdorff n X) hX.quadratic)
    (V : ℕ → X → Euclidean n)
    (w f : ℕ → SobolevSpace (hausdorff n X) hX.quadratic)
    (model : EuclideanHarmonicModel n S) : Prop where
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.EuclideanHarmonicModel
def OAI.RegularPointCoordinates.LocalPoissonHarmonicCompactnessInput line 65
Source documentation
A bounded-Laplacian radial sequence and an arbitrary bounded harmonic sequence have joint local limits. All assumptions are analytic bounds; the projected Euler equation is deliberately absent.
```
def LocalPoissonHarmonicCompactnessInput {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD