ApproximationRestriction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Restricting a pointed approximation to a smaller ball

theorem OAI.RegularPointCoordinates.IsPointedApproximation.restrict_radius line 13

Source documentation

Restriction costs a factor three in the approximation error because the preimage supplied by density must be shown to lie in the smaller ball.

theorem IsPointedApproximation.restrict_radius {X Y : Type*}
    [MetricSpace X] [MetricSpace Y] {p : X} {q : Y} {r R S ε : ℝ}
    (hr : 0 < r) (hS : 0 ≤ S) (hSR : S ≤ R) (hε : 0 ≤ ε)
    {f : X → Y} (hf : IsPointedApproximation p q r R ε f) :
    IsPointedApproximation p q r S (3 * ε) f := by
…

Mentions: OAI.RegularPointCoordinates.IsPointedApproximation