A measurable space structure on the type of continuous maps

In this file we endow the type C(X, Y) of continuous maps from X to Y with the Borel sigma-algebra coming from the compact-open topology. We show that, under some assumptions on X and Y, this is equal to the restriction of the product sigma-algebra over X → Y. This means that a function g : Z → C(X, Y) is measurable if and only if, for all x : X, z ↦ g z x is measurable. We then use this to build a measurable equivalence between {f : X → Y // Continuous f} and C(X, Y).

Main definition

• MeasurableEquiv.continuousMapToFun X Y: A measurable equivalence between C(X, Y) and {f : X → Y // Continuous f}.

Main statements

• borel_eq_iSup_comap_eval: The sigma-algebra over C(X, Y) is the coarsest that makes the maps f ↦ f x measurable for all x : X.
• measurable_iff_eval: A function g : Z → C(X, Y) is measurable if and only if, for all x : X, z ↦ g z x is measurable.

References

• https://math.stackexchange.com/questions/4789531/when-does-the-borel-sigma-algebra-of-compact-convergence-coincide-with-the-pr

Tags

continuous map, sigma-algebra

@[instance_reducible]

instance ContinuousMap.measurableSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] : MeasurableSpace C(X, Y)

Equations

• ContinuousMap.measurableSpace = borel C(X, Y)

instance instBorelSpaceContinuousMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] : BorelSpace C(X, Y)

theorem ContinuousMap.measurable_eval {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] (x : X) : Measurable fun (f : C(X, Y)) => f x

theorem ContinuousMap.iSup_comap_le_borel {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] : ⨆ (x : X), MeasurableSpace.comap (fun (f : C(X, Y)) => f x) (borel Y) ≤ borel C(X, Y)

The coarsest sigma-algebra over C(X, Y) making the evaluation maps f ↦ f x is smaller than the Borel sigma-algebra coming from the compact-open topology.

theorem ContinuousMap.borel_eq_iSup_comap_eval {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology X] [SecondCountableTopology Y] [LocallyCompactSpace X] [RegularSpace Y] : borel C(X, Y) = ⨆ (x : X), MeasurableSpace.comap (fun (f : C(X, Y)) => f x) (borel Y)

The sigma-algebra over C(X, Y) is the coarsest that makes the maps f ↦ f x measurable for all x : X.

The proof follows the one presented on https://math.stackexchange.com/questions/4789531/when-does-the-borel-sigma-algebra-of-compact-convergence-coincide-with-the-pr.

theorem ContinuousMap.measurableSpace_eq_iSup_comap_eval {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology X] [SecondCountableTopology Y] [LocallyCompactSpace X] [RegularSpace Y] [mY : MeasurableSpace Y] [BorelSpace Y] : measurableSpace = ⨆ (a : X), MeasurableSpace.comap (fun (b : C(X, Y)) => b a) mY

theorem ContinuousMap.measurable_iff_eval {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology X] [SecondCountableTopology Y] [LocallyCompactSpace X] [RegularSpace Y] [mY : MeasurableSpace Y] [BorelSpace Y] {Z : Type u_3} [MeasurableSpace Z] {g : Z → C(X, Y)} : Measurable g ↔ ∀ (x : X), Measurable fun (a : Z) => (g a) x

A function g : Z → C(X, Y) is measurable if and only if, for all x : X, z ↦ g z x is measurable.

def MeasurableEquiv.continuousMapToFun (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology X] [SecondCountableTopology Y] [LocallyCompactSpace X] [RegularSpace Y] [MeasurableSpace Y] [BorelSpace Y] : C(X, Y) ≃ᵐ { f : X → Y // Continuous f }

A measurable equivalence between C(X, Y) and {f : X → Y // Continuous f}.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasurableEquiv.continuousMapToFun_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology X] [SecondCountableTopology Y] [LocallyCompactSpace X] [RegularSpace Y] [MeasurableSpace Y] [BorelSpace Y] (f : C(X, Y)) : (continuousMapToFun X Y) f = ⟨⇑f, ⋯⟩

@[simp]

theorem MeasurableEquiv.symm_continuousMapToFun_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology X] [SecondCountableTopology Y] [LocallyCompactSpace X] [RegularSpace Y] [MeasurableSpace Y] [BorelSpace Y] (f : { g : X → Y // Continuous g }) : (continuousMapToFun X Y).symm f = { toFun := ↑f, continuous_toFun := ⋯ }

theorem MeasurableEquiv.continuousMapToFun_apply_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology X] [SecondCountableTopology Y] [LocallyCompactSpace X] [RegularSpace Y] [MeasurableSpace Y] [BorelSpace Y] (f : C(X, Y)) (x : X) : ↑((continuousMapToFun X Y) f) x = f x

theorem MeasurableEquiv.symm_continuousMapToFun_apply_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology X] [SecondCountableTopology Y] [LocallyCompactSpace X] [RegularSpace Y] [MeasurableSpace Y] [BorelSpace Y] (f : { g : X → Y // Continuous g }) (x : X) : ((continuousMapToFun X Y).symm f) x = ↑f x