UniformCenteredFits.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Centered radial fits with constants independent of the center and scale

theorem OAI.RegularPointCoordinates.canonical_centered_fits_of_squared_bound_uniform line 18

Source documentation

The centered-fit constant is fixed before the root radius, center, source, harmonic map, frame, defect sequence, and splitting error.

theorem canonical_centered_fits_of_squared_bound_uniform {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 2) X) [IsFiniteMeasureOnCompacts (hausdorff (m + 2) X)]
    (hmean : LocalHarmonicL2MeanValueInput hX) {κ₀ deltaCap Z : ℝ}
    (hκ₀ : 0 ≤ κ₀) (hcap : 0 ≤ deltaCap) (hZ : 0 < Z) :
    ∃ D : ℝ, 0 < D ∧ ∀ {a κ r0 B J C L δ ε : ℝ} {p : X},
    ∀ (_ha : 0 ≤ a) (_hδ : 0 ≤ δ) (_hδcap : δ ≤ deltaCap)
    (_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)
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn