OAI/Geometry/RCD/Coordinates/FramedRadialSmallness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.framed_covector_fit_smallness line 19

   Source documentation

   Normalizing and centering are used only to estimate the error. The result is the actual affine-fit error for the original map and covector.

   theorem DyadicDistanceReplacements.framed_covector_fit_smallness
       {n : ℕ} {κ r0 B J C : ℝ} {p : X} {S : DyadicDistanceSources μ hQ n κ p r0}
       (T : DyadicDistanceReplacements μ hQ S B J C) (i : ℕ)
       {ε Cχ : ℝ} (hε : 0 ≤ ε) (hε1 : ε ≤ 1) (hCχ : 0 ≤ Cχ)
       (u : Fin n → SobolevSpace μ hQ) (A : Euclidean n ≃L[ℝ] Euclidean n)
       (v : X → Euclidean n)
       (hfirst : FirstOrderSplittingOn μ hQ p (4 * (distanceSourceRadius r0 i / 64)) ε
         (transformedColumn μ hQ u A) v)
       (hmetric : IsPointedApproximation p 0 (distanceSourceRadius r0 i / 64) 4 ε
         (fun x => (distanceSourceRadius r0 i / 64)⁻¹ • (v x - v p)))
       (η : SobolevSpace μ hQ)
       (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict (ball p (4 * (distanceSourceRadius r0 i / 64)))]
   …

   Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.distanceSourceRadius, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.IsPointedApproximation, OAI.RegularPointCoordinates.SobolevSpace.toLp