RadialFitSmallness.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Passing the actual radial approximation to its least-squares error

theorem OAI.RegularPointCoordinates.radialFitError_sq_le_linear line 20

Source documentation

Any actual linear coordinate approximation bounds the affine fit. This transfers the proved radial L2 smallness to the dimensionless errors used in the dyadic recurrence.

theorem radialFitError_sq_le_linear {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (p : X) (r : ℝ) (hfin : μ (Metric.ball p r) ≠ ∞)
    (q a : SobolevSpace μ hQ) {B E : ℝ}
    (ha : ∀ᵐ x ∂μ.restrict (Metric.ball p r), localGamma μ hQ a a x ≤ B)
    (b : Euclidean n)
    (herror : (∫ x in Metric.ball p r, (localGamma μ hQ q a x -
      SobolevSpace.toLp μ hQ (sobolevColumnMap μ hQ u b) x) ^ 2 ∂μ) ≤ E) :
    (radialFitError μ hQ u p r hfin q a ha) ^ 2 ≤
      ((μ.real (Metric.ball p r))⁻¹ * E) / r ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.radialFitError