MeasurablePointedApproximation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Measurable representatives of pointed metric approximations

A finite net and the first admissible index replace an arbitrary pointed approximation by a measurable one, with a controlled loss in its error.

theorem OAI.RegularPointCoordinates.exists_measurable_net_choice line 21

Source documentation

A compact set admits a measurable nearest-net choice at any positive accuracy. No measurability of a subsequent map on the net is needed.

theorem exists_measurable_net_choice {s : Set X} (hs : IsCompact s)
    (hne : s.Nonempty) {η : ℝ} (hη : 0 < η) :
    ∃ c : ℕ → X, ∃ j : X → ℕ, Measurable j ∧
      ∀ x ∈ s, c (j x) ∈ s ∧ dist x (c (j x)) < η := by
…

theorem OAI.RegularPointCoordinates.IsPointedApproximation.exists_measurable line 51

Source documentation

Pointed approximations can be chosen measurable at the price of a fixed error factor. This concerns the actual maps on the whole space.

theorem IsPointedApproximation.exists_measurable {Y : Type*}
    [MetricSpace Y] [MeasurableSpace Y] {p : X} {q : Y} {r R ε : ℝ}
    (hr : 0 < r) (hR : 0 < R) (hε : 0 < ε) {f : X → Y}
    (hf : IsPointedApproximation p q r R ε f) :
    ∃ g : X → Y, Measurable g ∧ IsPointedApproximation p q r R (5 * ε) g := by
…

Mentions: OAI.RegularPointCoordinates.IsPointedApproximation