map_mul_eq_map_mconv_map' — Mathlib

English

Another form of independence for quotients under iIndepFun with AEMeasurability assumptions.

Русский

Другая форма независимости дробей при iIndepFun и AEMeasurability.

LaTeX

$$$\\forall i,j,k,l,\\ Ne(i,k) \\land Ne(i,l) \\land Ne(j,k) \\land Ne(j,l)\\Rightarrow IndepFun(\\frac{f_i}{f_j}, \\frac{f_k}{f_l})\\mu$$$

Lean4

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

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