mutuallySingular_map — Mathlib

English

If μ ⟂ ν, then the pushforward measures μ.map f and ν.map f are mutually singular when f is a measurable embedding.

Русский

Если μ ⟂ₘ ν, тоображенные по измеримому вложению f меры μ.map f и ν.map f взаимно-сингуларны.

LaTeX

$$$$ \\mu \\perp_{m} \\nu \\;\Rightarrow\\; (\\mathrm{map}\; f\,\\mu) \\perp_{m} (\\mathrm{map}\\, f\,\\nu) \quad\\text{при достаточном вложении } f. $$$$

Lean4

theorem _root_.MeasurableEmbedding.mutuallySingular_map {β : Type*} {_ : MeasurableSpace β} {f : α → β}
    (hf : MeasurableEmbedding f) (hμν : μ ⟂ₘ ν) : μ.map f ⟂ₘ ν.map f :=
  by
  refine ⟨f '' hμν.nullSet, hf.measurableSet_image' hμν.measurableSet_nullSet, ?_, ?_⟩
  · rw [hf.map_apply, hf.injective.preimage_image, hμν.measure_nullSet]
  · rw [hf.map_apply, Set.preimage_compl, hf.injective.preimage_image, hμν.measure_compl_nullSet]

Похожие утверждения