The Borel graph theorem

A map between standard Borel spaces is measurable if and only if its graph is measurable, and a map between Polish spaces is measurable if and only if its graph is analytic. One direction holds for every countably separated target (Measurable.measurableSet_graph); this file proves the converses.

The measurable form is the Lusin–Souslin theorem. If G ⊆ X × Y is a measurable set with at most one point above each x (InjOn Prod.fst G), the projection G → X is a measurable injection from a standard Borel space, hence a measurable embedding (MeasurableSet.measurableEmbedding_domRestrict_fst). So a map into X × Y with values in G is measurable as soon as its first coordinate is (MeasurableSet.measurable_iff_measurable_fst). Applied to x ↦ (x, f x), this recovers f from its graph. The same argument applies to maps defined on a subset s ⊆ X: the graph s.graphOn f is measurable if and only if s is measurable and f is measurable on s (TauCeti.measurableSet_graphOn_iff). When Y is nonempty, every set G with InjOn Prod.fst G is of the form graphOn f (Prod.fst '' G) (Set.exists_eq_graphOn_image_fst), so this describes all measurable sets with at most one point in each vertical section: their domain is measurable (MeasurableSet.of_graphOn) and the partial function they name is measurable on it (MeasurableSet.measurable_domRestrict_of_graphOn). The projection embedding above needs no such hypothesis. Without extending outside the domain, Set.InjOn.graphValue names the partial function even when Y is empty; Set.InjOn.measurable_graphValue proves it measurable. The measurable equivalence MeasurableSet.graphDomainEquiv identifies G with Prod.fst '' G by first projection, with inverse x ↦ (x, graphValue x).

The analytic form is Souslin's theorem. If the graph of f is analytic, the preimage f ⁻¹' t = (Function.graph f).preimage t of a Borel set is analytic, and so is the preimage of its complement; a set that is analytic with analytic complement is Borel.

Main results

• MeasurableSet.measurableEmbedding_domRestrict_fst: the projection of a measurable set with at most one point above each x is a measurable embedding.
• MeasurableSet.measurable_iff_measurable_fst: a map with values in such a set is measurable if and only if its first coordinate is.
• Set.InjOn.measurable_graphValue: the function defined by a functional Borel graph is measurable on its domain, with no nonemptiness assumption.
• MeasurableSet.graphDomainEquiv: a functional Borel graph is measurably equivalent to its domain by first projection.
• TauCeti.measurableSet_graphOn_iff: a partial map between standard Borel spaces has measurable graph if and only if its domain is measurable and it is measurable on its domain.
• TauCeti.measurableSet_graph_iff_measurable: a map between standard Borel spaces is measurable if and only if its graph is measurable.
• MeasureTheory.AnalyticSet.measurable_of_graph, TauCeti.analyticSet_graph_iff_measurable: a map between Polish spaces is measurable if and only if its graph is analytic.

References

• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer, 1995, Theorem 14.12 (the Borel graph theorem) and Theorem 15.1 (Lusin–Souslin).
• The statements of MeasureTheory.AnalyticSet.measurable_of_graph and TauCeti.analyticSet_graph_iff_measurable follow measurable_of_analyticSet_graph and analyticSet_graph_iff_measurable in Mathlib PR 41945, feat(Polish): add analyticSet_graph_iff_measurable (generantao, with Zelong Li, Aaron Liu and Wojciech Nawrocki), whose proof of the analytic direction is adapted here.
• The treatment of measurable sets with at most one point above each x through the projection embedding is adapted from InfinitaryLogic/Descriptive/BorelFunctionalGraph.lean in cameronfreer/infinitary-logic (Apache-2.0), which bundles these sets in a structure.

theorem MeasurableSet.measurableEmbedding_domRestrict_fst {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {G : Set (X × Y)} (hG : MeasurableSet G) (hinj : Set.InjOn Prod.fst G) : MeasurableEmbedding (G.domRestrict Prod.fst)

Lusin–Souslin for vertical sections. If a measurable subset G of a product of standard Borel spaces has at most one point above each x, its projection G → X is a measurable embedding.

theorem MeasurableSet.measurable_iff_measurable_fst {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {Z : Type u_3} [MeasurableSpace Z] {G : Set (X × Y)} (hG : MeasurableSet G) (hinj : Set.InjOn Prod.fst G) {φ : Z → X × Y} (hφ : ∀ (z : Z), φ z ∈ G) : Measurable φ ↔ Measurable fun (z : Z) => (φ z).1

A map with values in a measurable subset G of a product of standard Borel spaces with at most one point above each x is measurable if and only if its first coordinate is.

theorem Set.InjOn.measurable_graphValue {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {G : Set (X × Y)} (hinj : InjOn Prod.fst G) (hG : MeasurableSet G) : Measurable hinj.graphValue

The function defined by a functional Borel graph is measurable on its domain.

noncomputable def MeasurableSet.graphDomainEquiv {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {G : Set (X × Y)} (hG : MeasurableSet G) (hinj : Set.InjOn Prod.fst G) : ↑G ≃ᵐ ↑(Prod.fst '' G)

First projection identifies a functional Borel graph measurably with its domain.

@[simp]

theorem MeasurableSet.graphDomainEquiv_apply {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {G : Set (X × Y)} (hG : MeasurableSet G) (hinj : Set.InjOn Prod.fst G) (p : ↑G) : (hG.graphDomainEquiv hinj) p = ⟨(↑p).1, ⋯⟩

The domain equivalence is the first projection.

@[simp]

theorem MeasurableSet.graphDomainEquiv_symm_apply {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {G : Set (X × Y)} (hG : MeasurableSet G) (hinj : Set.InjOn Prod.fst G) (x : ↑(Prod.fst '' G)) : (hG.graphDomainEquiv hinj).symm x = ⟨(↑x, hinj.graphValue x), ⋯⟩

The inverse of the domain equivalence evaluates the function defined by the graph.

theorem MeasurableSet.of_graphOn {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {s : Set X} {f : X → Y} (h : MeasurableSet (Set.graphOn f s)) : MeasurableSet s

The domain of a measurable graph is measurable. If the graph of f on s is a measurable subset of a product of standard Borel spaces, then s is measurable.

theorem MeasurableSet.measurable_domRestrict_of_graphOn {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {s : Set X} {f : X → Y} (h : MeasurableSet (Set.graphOn f s)) : Measurable (s.domRestrict f)

A partial map with measurable graph is measurable on its domain. If the graph of f on s is a measurable subset of a product of standard Borel spaces, then f is measurable on s.

theorem TauCeti.measurableSet_graphOn_iff {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {s : Set X} {f : X → Y} : MeasurableSet (Set.graphOn f s) ↔ MeasurableSet s ∧ Measurable (s.domRestrict f)

The Borel graph theorem for partial maps. The graph of f on s, for standard Borel spaces X and Y, is measurable if and only if s is measurable and f is measurable on s.

theorem TauCeti.measurableSet_graph_iff_measurable {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {f : X → Y} : MeasurableSet (Function.graph f) ↔ Measurable f

The Borel graph theorem. A map between standard Borel spaces is measurable if and only if its graph is measurable.

theorem MeasureTheory.AnalyticSet.measurable_of_graph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [OpensMeasurableSpace X] [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] {f : X → Y} (hf : AnalyticSet (Function.graph f)) : Measurable f

Souslin's theorem for graphs. A map from a Hausdorff space with its Borel sets measurable to a Polish space, whose graph is analytic, is measurable.

theorem TauCeti.analyticSet_graph_iff_measurable {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] {f : X → Y} : MeasureTheory.AnalyticSet (Function.graph f) ↔ Measurable f

The Borel graph theorem, analytic form. A map between Polish spaces is measurable if and only if its graph is analytic.