RegularSharpSources.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The sharp estimate with its actual summable two-center source

theorem OAI.RegularPointCoordinates.regular_sharp_projection_actual_sources line 19
Source documentation
Both radial envelopes and both original Poisson defects are absorbed by the explicitly constructed positive source; its square sum is controlled by the same neighborhood tolerances.
```
theorem regular_sharp_projection_actual_sources {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 2) X) [(hausdorff (m + 2) X).Regular]
    (hgradient : LocalHarmonicL2GradientInput hX) (hmean : LocalHarmonicL2MeanValueInput hX)
    (hmeasured : LocalMeasuredCoordinateInput hX)
    (hhessian : LocalPoissonHessianActionInput hX)
    (hproduct : LocalPoissonGradientProductInput hX)
    (hpoincare : LocalMeanPoincareInput hX)
    (hcompact : LocalPoissonHarmonicCompactnessInput hX)
    {κ B J C A Cχ epsilon D : ℝ}
    (hκ : 0 ≤ κ) (hK : -κ ≤ K) (hB : 0 ≤ B) (hJ : 0 ≤ J) (hCχ : 0 ≤ Cχ) (hA : 0 ≤ A)
    (hepsilon : 0 ≤ epsilon)
    (hsmall : ((m + 2 : ℕ) : ℝ) ^ 2 *
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput, OAI.RegularPointCoordinates.LocalMeasuredCoordinateInput, OAI.RegularPointCoordinates.LocalPoissonHessianActionInput, OAI.RegularPointCoordinates.LocalPoissonGradientProductInput, OAI.RegularPointCoordinates.LocalMeanPoincareInput, OAI.RegularPointCoordinates.LocalPoissonHarmonicCompactnessInput