indepFun_div_left — Mathlib

English

Symmetric variant: if f_i is independent of f_j / f_k, then f_i is independent of f_j divided by f_k.

Русский

Симметричный вариант: независимость f_i от f_j / f_k переносится на f_i от f_j и f_k.

LaTeX

$$$\IndepFun (f_i) (f_j / f_k) κ μ$$$

Lean4

@[to_additive]
theorem indepFun_div_left (hf_indep : iIndepFun f κ μ) (hf_meas : ∀ i, Measurable (f i)) (i j k : ι) (hik : i ≠ k)
    (hjk : j ≠ k) : IndepFun (f i / f j) (f k) κ μ :=
  by
  have : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ := hf_indep.indepFun_prodMk hf_meas i j k hik hjk
  simpa using this.comp (measurable_fst.div measurable_snd) measurable_id

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