OAI/Geometry/RCD/Coordinates/RadialFitFromCorrection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.radial_fit_of_harmonic_correction line 19

   Source documentation

   A proved integral error for the actual radial pairing yields its least-squares contraction, with the exact restriction volume factor.

   theorem radial_fit_of_harmonic_correction
       (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic)
       (p : X) {r θ : ℝ} (hr : 0 < r) (hθ : 0 < θ) (hθ1 : θ ≤ 1)
       (hu : ∀ i, IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p r) (u i))
       (η : SobolevSpace (hausdorff n X) hX.quadratic)
       (hη : IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p r) η)
       (hηone : SobolevSpace.restrictLp (hausdorff n X) hX.quadratic (ball p r) η =
         restrictedOne (hausdorff n X) (ball p r) (ne_of_lt (hX.finiteOnBounded _ isBounded_ball)))
       (hfit : HasNormalizedAffineImprovement hX u p r θ)
       (q a h : SobolevSpace (hausdorff n X) hX.quadratic)
       {B error : ℝ} (he : 0 ≤ error)
       (ha : ∀ᵐ x ∂(hausdorff n X).restrict (ball p r),
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.restrictedOne, OAI.RegularPointCoordinates.HasNormalizedAffineImprovement