UniformRadialMatrices.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

One set of constants for all actual radial matrices

theorem OAI.RegularPointCoordinates.dyadic_radial_matrices_uniform line 19

Source documentation

The matrix and residual estimates use constants chosen before the root, center, coordinates and splitting error.

theorem dyadic_radial_matrices_uniform {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 2) X) [IsFiniteMeasureOnCompacts (hausdorff (m + 2) X)]
    (hhessian : LocalPoissonHessianInput hX) (hmean : LocalHarmonicL2MeanValueInput hX)
    (hgradient : LocalHarmonicL2GradientInput hX)
    {B J A Cχ κ₀ : ℝ} {d : ℕ} (hB : 0 ≤ B) (hJ : 0 ≤ J) (hA : 0 ≤ A)
    (hCχ : 0 ≤ Cχ) (hκ₀ : 0 ≤ κ₀) (hd : 0 < d) :
    ∃ Cg D Ca : ℝ, 1 ≤ Cg ∧ 0 < D ∧ 1 ≤ Ca ∧ ∀ {a κ r0 C L δ ε : ℝ} {p : X},
    ∀ (_ha : 0 ≤ a) (_hκ : 0 ≤ κ) (_hK : -κ ≤ K)
    (_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)
…

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