English
If f and g are independent and AE-measurable, and φ, ψ are AE-measurable with μ.map f and μ.map g respectively, then φ ∘ f and ψ ∘ g are independent with respect to μ.
Русский
Если f и g независимы и являются AE-измеримыми, а φ и ψ AE-измеримы относительно μ.map f и μ.map g соответственно, то φ ∘ f и ψ ∘ g независимы относительно μ.
LaTeX
$$$ \\operatorname{IndepFun}(f,g,\\mu) \\rightarrow \\operatorname{AEMeasurable}(f,\\mu) \\rightarrow \\operatorname{AEMeasurable}(g,\\mu) \\\\rightarrow \\operatorname{AEMeasurable}(\\varphi,\\mu\\map f) \\rightarrow \\operatorname{AEMeasurable}(\\psi,\\mu\\map g) \\\\rightarrow \\operatorname{IndepFun}(\\varphi \\circ f,\\ \\psi \\circ g) \\,\\mu $$$
Lean4
theorem comp₀ {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} {_mγ : MeasurableSpace γ}
{_mγ' : MeasurableSpace γ'} {φ : β → γ} {ψ : β' → γ'} (hfg : IndepFun f g μ) (hf : AEMeasurable f μ)
(hg : AEMeasurable g μ) (hφ : AEMeasurable φ (μ.map f)) (hψ : AEMeasurable ψ (μ.map g)) :
IndepFun (φ ∘ f) (ψ ∘ g) μ :=
Kernel.IndepFun.comp₀ hfg (by simp [hf]) (by simp [hg]) (by simp [hφ]) (by simp [hψ])
