indepFun_div_left — Mathlib

English

Let {f_i} be a family of measurable random variables forming a CondIndepFun structure. For indices i, j, k with i ≠ k and j ≠ k, the pair (f_i / f_j) and f_k are independent in the conditional sense.

Русский

Пусть {f_i} образуют структуру CondIndepFun. Для i, j, k с i ≠ k и j ≠ k пары (f_i / f_j) и f_k независимы условно.

LaTeX

$$$\forall i,j,k,\; i \neq k \land j \neq k \Rightarrow\; \text{CondIndepFun } m' hm' (f_i / f_j) \; (f_k) \; μ.$$$

Lean4

@[to_additive]
theorem indepFun_div_left (hf_indep : iCondIndepFun m' hm' f μ) (hf_meas : ∀ i, Measurable (f i)) (i j k : ι)
    (hik : i ≠ k) (hjk : j ≠ k) : CondIndepFun m' hm' (f i / f j) (f k) μ :=
  Kernel.iIndepFun.indepFun_div_left hf_indep hf_meas i j k hik hjk

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