UniformRadialCoefficient.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform constants for the actual radial coefficient estimates

theorem OAI.RegularPointCoordinates.dyadic_radial_coefficient_bound_uniform line 17

Source documentation

The coefficient constant precedes the center, root, coordinate map and splitting tolerance.

theorem dyadic_radial_coefficient_bound_uniform {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 2) X) [IsFiniteMeasureOnCompacts (hausdorff (m + 2) X)]
    (hgradient : LocalHarmonicL2GradientInput hX) {κ₀ : ℝ} (hκ₀ : 0 ≤ κ₀) :
    ∃ Ca : ℝ, 1 ≤ Ca ∧ ∀ {a κ r0 B J C Cχ L δ ε D : ℝ} {p : X},
    ∀ (_ha : 0 ≤ a) (_hCχ : 0 ≤ Cχ) (_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