OAI/Geometry/RCD/Coordinates/FramedDyadicFit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.actual_framed_dyadic_radial_fit line 17

   Source documentation

   The affine residual is the original one at both scales; the source uses only the covector norm in the current exact normalizing frame.

   theorem actual_framed_dyadic_radial_fit {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [IsFiniteMeasureOnCompacts (hausdorff n X)]
       (hn : 2 ≤ n) (hhessian : LocalPoissonHessianInput hX)
       {κ r0 B J C A epsilon Cχ : ℝ} (hκ : 0 ≤ κ) (hK : -κ ≤ K)
       (hB : 0 ≤ B) (hJ : 0 ≤ J) (hA : 0 ≤ A) (hepsilon : 0 ≤ epsilon) (hCχ : 0 ≤ 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 : ℕ)
       (hs1 : distanceSourceRadius r0 i ≤ 1)
       (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic)
       (F : Euclidean n ≃L[ℝ] Euclidean n)
       (hu : ∀ j, IsSobolevHarmonicOn (hausdorff n X) hX.quadratic
         (ball p (distanceSourceRadius r0 i / 4)) (transformedColumn (hausdorff n X) hX.quadratic u F j))
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalPoissonHessianInput, OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.distanceSourceRadius, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.transformedColumn