Continuous functions and the product σ-algebra

A continuous function on a product need not be measurable for the product of the Borel σ-algebras: that σ-algebra can be smaller than the Borel σ-algebra of the product. Nevertheless, a continuous function with values in a metrizable space is product-measurable when both factors are σ-compact and the second is Hausdorff, or when the first is σ-compact and the second is compact without separation assumptions. Neither factor needs to be second countable.

We first treat a compact second factor. Currying gives a continuous map into the metrizable space of continuous functions on that factor. Its σ-compact range is separable; evaluation on this range is measurable by Mathlib's Carathéodory theorem MeasureTheory.measurable_uncurry_of_continuous_of_measurable. A countable compact cover of the second factor then gives the general result.

In particular, on a σ-compact Hausdorff topological group, the scalar function (x, y) ↦ f (y⁻¹ * x) is product-measurable for continuous real f. This supplies the continuous-generator step in measurable convolution arguments, without asserting that group multiplication itself is measurable for the product Borel σ-algebra.

We also record OpensMeasurableSpace.of_prod_left: if the product X × Y with a nonempty second factor is an OpensMeasurableSpace for the product σ-algebra, then so is X.

theorem Continuous.measurable_prod_of_sigmaCompact_of_compact {X : Type u_1} {Y : Type u_2} {E : Type u_3} [TopologicalSpace X] [SigmaCompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [MeasurableSpace X] [OpensMeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace Y] [TopologicalSpace E] [TopologicalSpace.MetrizableSpace E] [MeasurableSpace E] [BorelSpace E] {f : X × Y → E} (hf : Continuous f) : Measurable f

A continuous map from a product to a metrizable space is measurable for the product σ-algebra if the first factor is σ-compact and the second is compact. No separation assumption on either factor is needed.

theorem Continuous.measurable_prod_of_sigmaCompact {X : Type u_1} {Y : Type u_2} {E : Type u_3} [TopologicalSpace X] [SigmaCompactSpace X] [TopologicalSpace Y] [SigmaCompactSpace Y] [T2Space Y] [MeasurableSpace X] [OpensMeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace Y] [TopologicalSpace E] [TopologicalSpace.MetrizableSpace E] [MeasurableSpace E] [BorelSpace E] {f : X × Y → E} (hf : Continuous f) : Measurable f

A continuous map from a product of σ-compact spaces to a metrizable space is measurable for the product σ-algebra. Only the second factor needs to be Hausdorff. In particular this does not require equality of the product and Borel σ-algebras on the domain.

theorem OpensMeasurableSpace.of_prod_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [TopologicalSpace Y] [MeasurableSpace Y] [Nonempty Y] [OpensMeasurableSpace (X × Y)] : OpensMeasurableSpace X

If the product of two topological spaces, the second nonempty, has the Borel property OpensMeasurableSpace for the product σ-algebra, so does the first factor: an open set s is the preimage of the measurable open set s ×ˢ univ under x ↦ (x, b).