UniformSharpProjection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.RegularPointCoordinates.SharpProjectionFamily.uniform_bound line 19
Source documentation
The collected Poisson and projection estimates imply one constant and one threshold, uniformly over the center, dyadic scale and configuration. The proof constructs the countersequence rather than assuming compactness for a normalized projection residual.
```
theorem SharpProjectionFamily.uniform_bound {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
    {I : Type*} {S ρ : ℝ} (d : SharpProjectionFamily hX I S ρ)
    (hcompact : LocalPoissonHarmonicCompactnessInput hX)
    (hgradient : LocalHarmonicL2GradientInput hX) (hn : 2 ≤ n)
    (hS : 0 < S) (hρ : 0 < ρ) (hρS : ρ < S) :
    ∃ C : ℝ, 0 < C ∧ ∃ δ : ℝ, 0 < δ ∧
      ∀ i, d.error i < δ → d.size i ≤ C * d.source i := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.SharpProjectionFamily, OAI.RegularPointCoordinates.LocalPoissonHarmonicCompactnessInput, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput