SharpProjectionFamily.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The Poisson, normalization and radial transport estimates provide a common coordinate frame, residual bounds and an approximate Euler equation.

structure OAI.RegularPointCoordinates.SharpProjectionFamily line 22
Source documentation
The precise analytic data used in the sharp-projection contradiction. The residual is the actual orthogonal projection residual.
```
structure SharpProjectionFamily {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X)
    (I : Type*) (S ρ : ℝ) where
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD
def OAI.RegularPointCoordinates.SharpProjectionFamily.compactnessSequence line 98
Source documentation
The radial potentials and coordinates form a compactness sequence; the accompanying harmonic function is chosen to be zero.
```
def SharpProjectionFamily.compactnessSequence {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
    {I : Type*} {S ρ : ℝ} (d : SharpProjectionFamily hX I S ρ)
    (hgradient : LocalHarmonicL2GradientInput hX) (hn : 2 ≤ n) (hS : 0 < S)
    (t : ℕ → I) (ht : Tendsto (d.error ∘ t) atTop (𝓝 0)) : RadialCompactnessSequence hX S where
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.SharpProjectionFamily, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.RadialCompactnessSequence