indepFun_div_div — Mathlib

English

Under finite measures and finite kernels, independence of f and g is equivalent to equality of certain product measures involving the joint map (f,g) and the product of the marginals map f and g.

Русский

При конечных мерах и ядрах независимость f и g эквивалентна равенству определённых произведённых мер, связанных с совместным отображением (f,g) и произведением отображений marginals.

LaTeX

$$$\IndepFun f g κ μ \iff μ ⊗ κ.map (\lambda ω. (f ω, g ω)) = μ ⊗ (κ.map f × κ.map g)$$$

Lean4

@[to_additive]
theorem indepFun_div_div (hf_indep : iIndepFun f κ μ) (hf_meas : ∀ i, Measurable (f i)) (i j k l : ι) (hik : i ≠ k)
    (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : IndepFun (f i / f j) (f k / f l) κ μ :=
  (hf_indep.indepFun_prodMk_prodMk hf_meas i j k l hik hil hjk hjl).comp measurable_div measurable_div

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