CanonicalDyadicCenters.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual affine center sequence of each radial covector

theorem OAI.RegularPointCoordinates.canonical_dyadic_affine_centers line 20

Source documentation

Choose coefficients of the genuine orthogonal projections. Their center values tend to zero, and consecutive differences are controlled by the genuine radial-fit errors. No uniqueness of coefficients is needed.

theorem canonical_dyadic_affine_centers {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)
…