DyadicCenteredRadial.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Centered radial fits with the actual summable Poisson defect

theorem OAI.RegularPointCoordinates.dyadic_centered_radial_estimate line 18

Source documentation

The original distance replacements, common harmonic map and exact normalizing frames produce centered radial fits with the two-convolution Poisson envelope. No radial-fit estimate is assumed.

theorem dyadic_centered_radial_estimate {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 2) X) [IsFiniteMeasureOnCompacts (hausdorff (m + 2) X)]
    (hhessian : LocalPoissonHessianInput hX)
    {a κ r0 B J C A Cχ L δ : ℝ} {p : X}
    (ha : 0 ≤ a) (hκ : 0 ≤ κ) (hK : -κ ≤ K)
    (hB : 0 ≤ B) (hJ : 0 ≤ J) (hA : 0 ≤ A) (hCχ : 0 ≤ Cχ)
    (hr01 : r0 ≤ 1) (hscale : a * (3 * r0) ≤ 1)
    (hBG : BallVolumeComparison (hausdorff (m + 2) X) (comparisonModelVolume (m + 1) a))
    (S : DyadicDistanceSources (hausdorff (m + 2) X) hX.quadratic (m + 2) κ p r0)
    (T : DyadicDistanceReplacements (hausdorff (m + 2) X) hX.quadratic S B J C)
    (hP : Summable (normalizedPoissonDefect (hausdorff (m + 2) X) hX.quadratic S))
    (hquarter : ∀ t : ℝ, 0 < t → t ≤ r0 →
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalPoissonHessianInput, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.normalizedPoissonDefect

theorem OAI.RegularPointCoordinates.radial_fit_pinching_envelope_budget line 91
Source documentation
The envelope used above is summable with its original full Poisson budget. The two fixed geometric convolutions cost the explicit factor 64.
```
theorem radial_fit_pinching_envelope_budget {μ : Measure X} {hQ : QuadraticCheegerEnergy μ}
    [IsFiniteMeasureOnCompacts μ]
    {n : ℕ} {κ r0 Cχ δ : ℝ} {p : X}
    (S : DyadicDistanceSources μ hQ n κ p r0)
    (hκ : 0 ≤ κ) (hCχ : 0 ≤ Cχ) (hδ : 0 ≤ δ)
    (hP : Summable (normalizedPoissonDefect μ hQ S)) :
    let E := pinchingEnvelope (7 / 8) (3 / 4) (radialFitQualitativeConstant n Cχ * δ)
…
```
Mentions: OAI.RegularPointCoordinates.QuadraticCheegerEnergy, OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.normalizedPoissonDefect, OAI.RegularPointCoordinates.pinchingEnvelope, OAI.RegularPointCoordinates.radialFitQualitativeConstant