Graphs of measurable maps are measurable

The graph Function.graph f of a measurable map f : α → β is a measurable subset of α × β as soon as the diagonal of β is measurable (MeasurableEq β), since it is the preimage of the diagonal under (a, b) ↦ (f a, b). A countably separated measurable space has a measurable diagonal: the diagonal is the intersection, over a countable separating family of measurable sets s, of the sets of pairs that lie both in s or both outside it. In particular graphs of measurable maps into standard Borel spaces, or into quotients whose σ-algebra is countably separated, are measurable.

The same holds for maps defined on a measurable subset only: the graph s.graphOn f is measurable when s is measurable and the restriction s.domRestrict f is measurable.

These are the easy directions of the Borel graph theorem; the converses, which need the Lusin–Souslin theorem, are in TauCeti.MeasureTheory.Constructions.Polish.Graph.

Main results

• MeasurableSpace.measurableEq_of_countablySeparated: a countably separated measurable space has a measurable diagonal.
• Measurable.measurableSet_graph: the graph of a measurable map into a space with measurable diagonal is measurable.
• MeasurableSet.graphOn: the graph of a map that is measurable on a measurable set is measurable.

References

• The statement of Measurable.measurableSet_graph and the instance MeasurableSpace.measurableEq_of_countablySeparated follow Mathlib PR 41944, feat(CountablyGenerated): add measurableSet_graph (generantao and Wojciech Nawrocki).

@[instance 100]

instance MeasurableSpace.measurableEq_of_countablySeparated {α : Type u_1} [MeasurableSpace α] [CountablySeparated α] : MeasurableEq α

A countably separated measurable space has a measurable diagonal: the diagonal is the intersection of the measurable sets s ×ˢ s ∪ sᶜ ×ˢ sᶜ over a countable separating family.

theorem Measurable.measurableSet_graph {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableEq β] {f : α → β} (hf : Measurable f) : MeasurableSet (Function.graph f)

The graph of a measurable map into a space with measurable diagonal, for example a countably separated space, is measurable.

theorem MeasurableSet.graphOn {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableEq β] {s : Set α} {f : α → β} (hs : MeasurableSet s) (hf : Measurable (s.domRestrict f)) : MeasurableSet (Set.graphOn f s)

The graph of a map that is measurable on a measurable set s, into a space with measurable diagonal, is measurable.