map_mul_eq_map_mconv_map — Mathlib

English

If f and g are random variable mappings with independence, then the map of their product equals the product of maps in the Monoid sense.

Русский

Если отображения f и g независимы, то отображение произведения равно произведению отображений в монотной операции.

LaTeX

$$$\\text{For independent } f,g:\\map(f\\cdot g)=\\map f \\;\\otimes\\; \\map g$ (in the monoid sense).$$

Lean4

@[to_additive]
theorem map_mul_eq_map_mconv_map [IsFiniteMeasure μ] {f g : Ω → M} (hf : Measurable f) (hg : Measurable g)
    (hfg : IndepFun f g μ) : μ.map (f * g) = (μ.map f) ∗ₘ (μ.map g) :=
  hfg.map_mul_eq_map_mconv_map₀ hf.aemeasurable hg.aemeasurable

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