ProjectionMeasuredCoordinates.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual metric coordinates on the projection ball

theorem OAI.RegularPointCoordinates.radial_metric_from_controlled line 19
Source documentation
The controlled-normalization theorem uses a half-ball in units s/8. This is the same physical ball as the radial fit's radius-four ball in units s/64, with the exact corresponding error conversion.
```
theorem radial_metric_from_controlled {n : ℕ} {p : X} {s epsilon : ℝ}
    (hs : 0 < s) (V : X → Euclidean n)
    (hf : IsPointedApproximation p 0 (s / 8) (1 / 2) epsilon
      (fun x => (s / 8)⁻¹ • V x)) :
    IsPointedApproximation p 0 (s / 64) 4 (8 * epsilon)
      (fun x => (s / 64)⁻¹ • V x) := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation

theorem OAI.RegularPointCoordinates.projection_metric_rescale line 33

Source documentation

Restrict the centered metric map used by the radial fits and express it in the length units of the two-center projection.

theorem projection_metric_rescale {n : ℕ} {p : X} {s delta : ℝ}
    (hs : 0 < s) (hdelta : 0 ≤ delta) (f : X → Euclidean n) (hcenter : f p = 0)
    (hf : IsPointedApproximation p 0 (s / 64) 4 delta f) :
    IsPointedApproximation p 0 s (2 * (1 / 1024)) (delta / 32)
      (fun x => (1 / 64 : ℝ) • f x) := by
…

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

theorem OAI.RegularPointCoordinates.projection_measured_coordinates line 84

Source documentation

The published measured-convergence input applies to the same centered coordinates used by the radial argument, at the fixed projection radius.

theorem projection_measured_coordinates {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n)
    (hmeasured : LocalMeasuredCoordinateInput hX) {epsilon : ℝ} (hepsilon : 0 < epsilon) :
    ∃ delta : ℝ, 0 < delta ∧ ∀ (p : X) (s : ℝ), 0 < s →
      -delta / 32 ≤ K * s ^ 2 →
      ∀ f : X → Euclidean n, Measurable f → f p = 0 →
        IsPointedApproximation p 0 (s / 64) 4 delta f →
        IsMeasuredEuclideanApproximation (hausdorff n X) n p s (1 / 1024) epsilon
          (fun x => (1 / 64 : ℝ) • f x) := by
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalMeasuredCoordinateInput, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation, OAI.RegularPointCoordinates.IsMeasuredEuclideanApproximation, OAI.RegularPointCoordinates.hausdorff