indepFun_div_left₀ — Mathlib

English

Independence is preserved under pairwise division: if f is independent from g and h, then f / g is independent from h / i for appropriate indices.

Русский

Независимость сохраняется при попарном делении: если f независим от g и h, то f / g независим от h / i для подходящих индексов.

LaTeX

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

Lean4

@[to_additive]
theorem indepFun_div_left₀ (hf_indep : iIndepFun f κ μ) (hf_meas : ∀ i, AEMeasurable (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

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