CanonicalAffineDifference.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Center differences of the actual dyadic radial fits

theorem OAI.RegularPointCoordinates.canonical_affine_center_difference line 18

Source documentation

Both fits concern the same local radial derivative. The change of outer distance cutoff introduces no extra term in their center difference.

theorem canonical_affine_center_difference {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 L : ℝ} {p : X}
      (S : DyadicDistanceSources (hausdorff n X) hX.quadratic n κ p r0)
      (T : DyadicDistanceReplacements (hausdorff n X) hX.quadratic S B J C)
      (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic)
      (hbase : ∀ i j, ∀ᵐ x ∂(hausdorff n X).restrict (ball p (distanceSourceRadius r0 i / 64)),
        localGamma (hausdorff n X) hX.quadratic (u j) (u j) x ≤ L ^ 2)
      (v : X → Euclidean n) (i j : ℕ), i ≤ j →
      -κ₀ ≤ K * (distanceSourceRadius r0 j / 64) ^ 2 →
      (∀ k, IsSobolevHarmonicOn (hausdorff n X) hX.quadratic
…

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