CanonicalAffineCenter.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Center values of the actual least-squares radial fits

theorem OAI.RegularPointCoordinates.canonical_radial_affine_center_bound line 19

Source documentation

The published harmonic mean-value input bounds the center value of every actual radial fit by radius times the current covector norm. The same evaluation constant works for all source scales and centers.

theorem canonical_radial_affine_center_bound {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [IsFiniteMeasureOnCompacts (hausdorff n X)]
    (hmean : LocalHarmonicL2MeanValueInput hX) (hn : 2 ≤ n) {κ₀ : ℝ} (hκ₀ : 0 ≤ κ₀) :
    ∃ M : ℝ, 1 ≤ M ∧ ∀ {κ r0 B J C ε : ℝ} {p : X}
      (S : DyadicDistanceSources (hausdorff n X) hX.quadratic n κ p r0)
      (T : DyadicDistanceReplacements (hausdorff n X) hX.quadratic S B J C)
      (i : ℕ) (r : ℝ), 0 < r → r ≤ 4 * distanceSourceRadius r0 i → -κ₀ ≤ K * r ^ 2 → 0 ≤ ε →
    ∀ (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic) (v : X → Euclidean n),
      (∀ j, IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p r) (u j)) →
      ContinuousOn v (ball p r) →
      (∀ j, SobolevSpace.toLp (hausdorff n X) hX.quadratic (u j) =ᵐ[
        (hausdorff n X).restrict (ball p r)] fun x => v x j) →
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput, OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.distanceSourceRadius, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.toLp