OAI/Geometry/RCD/Coordinates/HarmonicFitStep.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.harmonic_affine_fit_step line 19

   Source documentation

   Harmonic improvement and a harmonic correction give the one-step fit estimate for a possibly nonharmonic L² target. The error is the actual correction norm and the restriction loss is the actual volume ratio.

   theorem harmonic_affine_fit_step
       (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 θ)
       (f : Lp ℝ 2 ((hausdorff n X).restrict (ball p r)))
       (h : SobolevSpace (hausdorff n X) hX.quadratic)
       (hh : IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p r) h) :
   …

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