CanonicalCenteredFits.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative removal of the actual affine constants

theorem OAI.RegularPointCoordinates.canonical_centered_fits_of_squared_bound line 19

Source documentation

The inward estimate and square summability control the canonical radial fits.

theorem canonical_centered_fits_of_squared_bound {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 2) X) [IsFiniteMeasureOnCompacts (hausdorff (m + 2) X)]
    (hmean : LocalHarmonicL2MeanValueInput hX) {a κ₀ κ r0 B J C L δ ε : ℝ} {p : X}
    (hκ₀ : 0 ≤ κ₀) (ha : 0 ≤ a) (hδ : 0 ≤ δ)
    (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)
    (u : Fin (m + 2) → SobolevSpace (hausdorff (m + 2) X) hX.quadratic)
    (v : X → Euclidean (m + 2))
    (hu : FirstOrderSplittingOn (hausdorff (m + 2) X) hX.quadratic p r0 ε u v)
    (hbase : ∀ i j, ∀ᵐ x ∂(hausdorff (m + 2) X).restrict (ball p (distanceSourceRadius r0 i / 64)),
      localGamma (hausdorff (m + 2) X) hX.quadratic (u j) (u j) x ≤ L ^ 2)
…