RecenterApproximation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Centering an unpointed Euclidean ball approximation

The image of the center is forced to be small by the eccentricity of a Euclidean ball. Translation therefore turns an ordinary ball approximation into a pointed approximation with an explicit error loss.

theorem OAI.RegularPointCoordinates.ballApproximation_center_norm_le line 19
theorem OAI.RegularPointCoordinates.IsBallApproximation.recenter line 52
Source documentation
Centering loses only a factor four in the approximation error.
```
theorem IsBallApproximation.recenter {X : Type*} [MetricSpace X] {n : ℕ}
    {p : X} {r R ε : ℝ} (hr : 0 < r) (hε : 0 ≤ ε) (hεR : ε < R)
    {f : X → Euclidean n} (hf : IsBallApproximation p 0 r R ε f) :
    IsPointedApproximation p 0 r R (4 * ε) (fun x => f x - f p) := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsBallApproximation, OAI.RegularPointCoordinates.IsPointedApproximation
theorem OAI.RegularPointCoordinates.IsPointedApproximation.rescale_four line 78
Source documentation
The half-ball conclusion at scale 4r is a radius-two conclusion at scale r. This fixed rescaling is used after volume almost rigidity.
```
theorem IsPointedApproximation.rescale_four {X : Type*} [MetricSpace X] {n : ℕ}
    {p : X} {r ε : ℝ} (hr : 0 < r) {f : X → Euclidean n}
    (hf : IsPointedApproximation p 0 (4 * r) (1 / 2) ε f) :
    IsPointedApproximation p 0 r 2 (4 * ε) (fun x => (4 : ℝ) • f x) := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation