DyadicRadialCoefficient.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Near-identity coefficient estimates for the actual centered radial fits

theorem OAI.RegularPointCoordinates.dyadic_radial_coefficient_bound line 21

Source documentation

The error of an actual centered fit bounds its coefficient error from the identity covector. The reference candidate is the original coordinate function, whose quantitative error has already been proved.

theorem dyadic_radial_coefficient_bound {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 2) X) [IsFiniteMeasureOnCompacts (hausdorff (m + 2) X)]
    (hgradient : LocalHarmonicL2GradientInput hX)
    {a κ r0 B J C Cχ L δ κ₀ ε D : ℝ} {p : X}
    (ha : 0 ≤ a) (hCχ : 0 ≤ Cχ) (hκ₀ : 0 ≤ κ₀) (hD : 0 ≤ D)
    (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)
    (hquarter : ∀ t : ℝ, 0 < t → t ≤ r0 →
      |(hausdorff (m + 2) X).real (ball p t) / (euclideanUnitVolume (m + 2) * t ^ (m + 2)) - 1| ≤ 1 / 4)
    (u : Fin (m + 2) → SobolevSpace (hausdorff (m + 2) X) hX.quadratic)
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.euclideanUnitVolume, OAI.RegularPointCoordinates.SobolevSpace