NormalizedRadialCandidate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative comparison with the original centered coordinate function

theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.normalized_radial_candidate line 21

Source documentation

The genuine radial derivative is close to the centered original coordinate function in the same inverse-frame norm used by the fits.

theorem DyadicDistanceReplacements.normalized_radial_candidate
    {n : ℕ} {κ r0 B J C omega δ Cχ : ℝ} {p : X}
    {S : DyadicDistanceSources μ hQ n κ p r0}
    (T : DyadicDistanceReplacements μ hQ S B J C) (i : ℕ)
    (homega : 0 < omega) (hδ : 0 ≤ δ)
    (hδ1 : radialNormalizationRestrictionConstant n * δ ≤ 1) (hCχ : 0 ≤ Cχ)
    (hquarter : ∀ t : ℝ, 0 < t → t ≤ 2 * distanceSourceRadius r0 i →
      |μ.real (ball p t) / (omega * t ^ n) - 1| ≤ 1 / 4)
    (u : Fin n → SobolevSpace μ hQ) (N : Euclidean n ≃L[ℝ] Euclidean n)
    (V W : X → Euclidean n)
    (hV : ContinuousOn V (ball p (2 * distanceSourceRadius r0 i)))
    (hu : ∀ j, SobolevSpace.toLp μ hQ (u j) =ᵐ[
…

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