Mutual singularity pulls back along a measurable map

Category: 1-Mathlib (CSD-free upstream candidates).

Measure.MutuallySingular.of_map — if the pushforwards of μ and ν along a measurable f : α → β are mutually singular, then μ and ν are mutually singular.

Why this is not already in Mathlib

Mathlib.MeasureTheory.Measure.MutuallySingular carries the forward direction, and only for embeddings: MeasurableEmbedding.mutuallySingular_map sends μ ⟂ₘ ν to μ.map f ⟂ₘ ν.map f, using injectivity to push a separating set forward through f '' ·.

The direction here goes the other way and needs no embedding hypothesis, because a separating set is pulled back rather than pushed forward: f ⁻¹' B is measurable whenever B is, preimage commutes with complement, and Measure.map_apply converts each mapped-measure statement into a statement about the preimage. Injectivity would be needed only to go forwards.

No finiteness, σ-finiteness or probability hypothesis is required.

Provenance

Staged as upstream Mathlib material; no CsdLean4-namespace content.

theorem MeasureTheory.Measure.MutuallySingular.of_map {α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {μ ν : Measure α} {f : α → β} (hf : Measurable f) (h : (map f μ).MutuallySingular (map f ν)) : μ.MutuallySingular ν

Mutual singularity pulls back along a measurable map. If f is measurable and the pushforwards f_* μ and f_* ν are mutually singular, then so are μ and ν.

The separating set is the preimage of the one separating the pushforwards.