OAI/Geometry/RCD/Coordinates/RadialFitRecurrence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.radialFitError_step_of_correction line 18

   Source documentation

   The harmonic correction gives a recurrence for the canonical actual fit errors, with the exact contraction and restriction-volume factors.

   theorem radialFitError_step_of_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 E : ℝ} (hE : 0 ≤ E)
       (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