map_mul_eq_map_mconv_map₀' — Mathlib

English

AEMeasurable version of the Div Div independence with iIndepFun: independence holds for quotients with AEMeasurable inputs.

Русский

Версия AEMеасurable для независимости дробей: независимость сохраняется при AEMeasurable входах.

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 : AEMeasurable f μ) (hg : AEMeasurable g μ)
    (σf : SigmaFinite (μ.map f)) (σg : SigmaFinite (μ.map g)) (hfg : IndepFun f g μ) :
    μ.map (f * g) = (μ.map f) ∗ₘ (μ.map g) :=
  by
  conv in f * g => change (fun x ↦ x.1 * x.2) ∘ (fun ω ↦ (f ω, g ω))
  rw [← measurable_mul.aemeasurable.map_map_of_aemeasurable (hf.prodMk hg),
    (indepFun_iff_map_prod_eq_prod_map_map' hf hg σf σg).mp hfg, Measure.mconv]

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