English
Let f and g be random-variable-valued maps on Ω with respect to a kernel κ and a measure μ, and let φ and ψ be measurable transformations on their respective codomains. If f and g are independent under κ and μ, then the composed variables φ ∘ f and ψ ∘ g are also independent under κ and μ.
Русский
Пусть f и g — случайные величины на Ω через ядро κ и меру μ, а φ и ψ — измеримые преобразования соответствующих кодоминов. Если f и g независимы относительно κ μ, то и φ ∘ f и ψ ∘ g независимы относительно κ μ.
LaTeX
$$$\IndepFun f g κ μ \;\; \Rightarrow \;\; \Measurable φ \;\land\; \Measurable ψ \;\Rightarrow \; \IndepFun (\phi \circ f) (\psi \circ g) κ μ$$$
Lean4
theorem comp {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {mγ : MeasurableSpace γ} {mγ' : MeasurableSpace γ'}
{φ : β → γ} {ψ : β' → γ'} (hfg : IndepFun f g κ μ) (hφ : Measurable φ) (hψ : Measurable ψ) :
IndepFun (φ ∘ f) (ψ ∘ g) κ μ := by
rintro _ _ ⟨A, hA, rfl⟩ ⟨B, hB, rfl⟩
apply hfg
· exact ⟨φ ⁻¹' A, hφ hA, Set.preimage_comp.symm⟩
· exact ⟨ψ ⁻¹' B, hψ hB, Set.preimage_comp.symm⟩
