Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

A measurable selection principle

Lax606786.MeasurableSelection · concepts/Lax606786/MeasurableSelection.lean · lax-606786

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Let (xn)(x_n) be a sequence in a measurable space YY and (Sn)(S_n) a cover of Ω\Omega by measurable sets. Then the first-index map N(ω)=min⁡{n:ω∈Sn}N(\omega) = \min\{n : \omega \in S_n\} is measurable, and so is ω↦xN(ω)\omega \mapsto x_{N(\omega)}.

    A map into a separable metric space is measurable as soon as its distance to every point is.

    Concept map
    1 concept
    100%
    Proven claimThis concept
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 measurable_of_countable_cover proven

    2 measurable_of_measurable_dist proven

    In the paper

    • page 3 of this submission's paper

    Lean source view on GitLab

    1import Mathlib.MeasureTheory.MeasurableSpace.Constructions
    2
    3import Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
    4/-!
    5---
    6title: A measurable selection principle
    7type: theorem
    8---
    9Let (xn)(x_n) be a sequence in a measurable space YY and (Sn)(S_n) a cover of Ω\Omega by measurable
    10sets. Then the first-index map N(ω)=min⁡{n:ω∈Sn}N(\omega) = \min\{n : \omega \in S_n\} is measurable, and so is
    11ω↦xN(ω)\omega \mapsto x_{N(\omega)}.
    12
    13A map into a separable metric space is measurable as soon as its distance to every point is.
    14-/
    15
    16namespace Lax606786.MeasurableSelection
    17
    18/-- The first index of a countable measurable cover is measurable. -/
    19axiom measurable_of_countable_cover {Ω Y : Type*} [MeasurableSpace Ω] [MeasurableSpace Y]
    20 (x : ℕ → Y) (S : ℕ → Set Ω) (hS : ∀ n, MeasurableSet (S n)) (hcover : (⋃ n, S n) = Set.univ) :
    21 ∃ N : Ω → ℕ, Measurable N ∧ Measurable (fun ω => x (N ω)) ∧
    22 ∀ ω, ω ∈ S (N ω) ∧ ∀ m, ω ∈ S m → N ω ≤ m
    23
    24/-- A map into a separable metric space is measurable when its distance to every point is. -/
    25axiom measurable_of_measurable_dist {Y Ω : Type*} [MetricSpace Y]
    26 [TopologicalSpace.SeparableSpace Y] [MeasurableSpace Y] [BorelSpace Y] [MeasurableSpace Ω] {F : Ω → Y}
    27 (h : ∀ y : Y, Measurable fun ω => dist (F ω) y) : Measurable F
    28
    29end Lax606786.MeasurableSelection
    30
    Show ProofShow Proof
    Builds on

    none

    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…