MetricQuadraticError.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Squared-distance value control from the actual metric approximation

theorem OAI.RegularPointCoordinates.IsPointedApproximation.centered_norm_error line 16

Source documentation

A centered metric approximation controls the actual coordinate norm.

theorem IsPointedApproximation.centered_norm_error {n : ℕ} {p : X} {r R ε : ℝ}
    (hr : 0 < r) (hR : 0 ≤ R) {f : X → Euclidean n}
    (hf : IsPointedApproximation p 0 r R ε f) (hfp : f p = 0)
    {x : X} (hx : dist x p ≤ R * r) :
    |‖f x‖ - dist x p / r| ≤ ε ∧ ‖f x‖ ≤ R + ε := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation

theorem OAI.RegularPointCoordinates.IsPointedApproximation.quadratic_value_error line 28

Source documentation

Squaring the norm incurs only the explicit factor coming from the bounded testing ball. This is the value estimate in radial convergence.

theorem IsPointedApproximation.quadratic_value_error {n : ℕ} {p : X} {r R ε : ℝ}
    (hr : 0 < r) (hR : 0 ≤ R) (hε : 0 ≤ ε) {f : X → Euclidean n}
    (hf : IsPointedApproximation p 0 r R ε f) (hfp : f p = 0)
    {x : X} (hx : dist x p ≤ R * r) :
    |dist p x ^ 2 / 2 - r ^ 2 * ‖f x‖ ^ 2 / 2| ≤
      r ^ 2 * (ε * (2 * R + ε) / 2) := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation