Documentation

TauCeti.MeasureTheory.MeasurableSpace.Selection

Measurable selections of closed-valued maps #

Let M assign to each point z of a measurable space a nonempty closed subset M z of a Polish space X. The Kuratowski–Ryll-Nardzewski theorem says that if M is weakly measurable, meaning that {z | M z ∩ U ≠ ∅} is measurable for every open U ⊆ X, then M has a measurable selection: a measurable map f with f z ∈ M z for every z. Unlike the Jankov–von Neumann theorem, which gives a selection measurable only for the σ-algebra generated by analytic sets, this selection is measurable for the given σ-algebra; for a Borel parameter space it is Borel.

The main application here is to minimizers depending continuously on a parameter. If F z x depends jointly continuously on (z, x), the parameter space carries its Borel σ-algebra, X is Polish and σ-compact, and F z attains its minimum for every z, then the minimizers can be chosen Borel measurably in z. Indeed the set of z for which F z has a minimizer in a fixed compact set is closed, and every open subset of X is a countable union of compact sets.

Main statements #

References #

theorem TauCeti.exists_measurable_forall_mem {Z : Type u_1} {X : Type u_2} [MeasurableSpace Z] [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] {M : Z → Set X} (hclosed : ∀ (z : Z), IsClosed (M z)) (hne : ∀ (z : Z), (M z).Nonempty) (hM : ∀ (U : Set X), IsOpen U → MeasurableSet {z : Z | (M z ∩ U).Nonempty}) :
∃ (f : Z → X), Measurable f ∧ ∀ (z : Z), f z ∈ M z

The Kuratowski–Ryll-Nardzewski measurable selection theorem. A map M from a measurable space to the nonempty closed subsets of a Polish space, which is weakly measurable in the sense that {z | M z ∩ U ≠ ∅} is measurable for every open U, has a measurable selection.

theorem Continuous.exists_measurable_isMinOn {Z : Type u_1} {X : Type u_2} [TopologicalSpace Z] [MeasurableSpace Z] [OpensMeasurableSpace Z] [TopologicalSpace X] [PolishSpace X] [SigmaCompactSpace X] [MeasurableSpace X] [BorelSpace X] {β : Type u_3} [Preorder β] [TopologicalSpace β] [OrderClosedTopology β] {F : Z → X → β} (hF : Continuous (Function.uncurry F)) (hmin : ∀ (z : Z), ∃ (x : X), IsMinOn (F z) Set.univ x) :
∃ (T : Z → X), Measurable T ∧ ∀ (z : Z), IsMinOn (F z) Set.univ (T z)

Measurable selection of minimizers. Let F z x depend jointly continuously on a parameter z, in a space whose open sets are measurable, and on x in a σ-compact Polish space. The values lie in a preorder with a closed order relation. If F z attains its minimum for every z, then a minimizer of F z can be chosen measurably in z. In particular, this applies when X is locally compact.