English
If two random-variable–valued functions f and g are conditionally independent, then composing f and g with measurable maps φ and ψ yields a new pair that is still conditionally independent.
Русский
Если две функции-случайные величины f и g условно независимы, то композиция f с одними измеримыми отображениями φ и ψ и композиция g с теми же отображениями образуют новую пару, которая остаётся условно независимой.
LaTeX
$$$\operatorname{CondIndepFun} \; m' \; hm' \; f \; g \; μ \Rightarrow \operatorname{CondIndepFun} \; m' \; hm' \; (\varphi \circ f) \; (\psi \circ g) \; μ$, при условии, что $\varphi$ и $\psi$ измеримы.$$
Lean4
theorem comp {γ γ' : Type*} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} {_mγ : MeasurableSpace γ}
{_mγ' : MeasurableSpace γ'} {φ : β → γ} {ψ : β' → γ'} (hfg : CondIndepFun m' hm' f g μ) (hφ : Measurable φ)
(hψ : Measurable ψ) : CondIndepFun m' hm' (φ ∘ f) (ψ ∘ g) μ :=
Kernel.IndepFun.comp hfg hφ hψ
