FramedRadialCandidate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual centered coordinate candidate for the radial fit

theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.framed_radial_candidate line 20

Source documentation

The qualitative radial estimate controls the specific original centered coordinate candidate, rather than just the best-fit infimum.

theorem DyadicDistanceReplacements.framed_radial_candidate
    {n : ℕ} {κ r0 B J C ε Cχ : ℝ} {p : X}
    {S : DyadicDistanceSources μ hQ n κ p r0}
    (T : DyadicDistanceReplacements μ hQ S B J C) (i : ℕ)
    (hε : 0 ≤ ε) (hε1 : ε ≤ 1) (hCχ : 0 ≤ Cχ)
    (u : Fin n → SobolevSpace μ hQ) (N : Euclidean n ≃L[ℝ] Euclidean n)
    (V W : X → Euclidean n)
    (hV : ContinuousOn V (ball p (4 * (distanceSourceRadius r0 i / 64))))
    (hu : ∀ j, SobolevSpace.toLp μ hQ (u j) =ᵐ[
      μ.restrict (ball p (4 * (distanceSourceRadius r0 i / 64)))] fun x => V x j)
    (hfirst : FirstOrderSplittingOn μ hQ p (4 * (distanceSourceRadius r0 i / 64)) ε
      (transformedColumn μ hQ u N) W)
…

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