English
If hfg expresses independence of f and g with respect to κ and μ, and f, g, φ, ψ are AE-measurable with respect to the appropriate pulled-back measures, then the composed pair φ ∘ f and ψ ∘ g is independent with respect to the same κ and μ.
Русский
Если существует независимость f и g относительно κ μ, и соответствующие композиции φ ∘ f и ψ ∘ g являются AE-измеримыми относительно соответствующих отображённых мер, то они сохраняют независимость относительно той же пары κ μ.
LaTeX
$$$\IndepFun f g κ μ \;\land\; \text{AE-measurable } f \; (κ \circ_ m μ) \land \text{AE-measurable } g \ (κ \circ_ m μ) \land\; \text{AE-measurable } φ ((κ \circ_ m μ).map f) \land\; \text{AE-measurable } ψ ((κ \circ_ m μ).map g) \Rightarrow \IndepFun (φ \circ f) (ψ \circ g) κ μ$$
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) κ μ :=
by
have h : IndepFun ((hφ.mk φ) ∘ f) ((hψ.mk ψ) ∘ g) κ μ := by refine IndepFun.comp hfg hφ.measurable_mk hψ.measurable_mk
have hφ_ae := ae_of_ae_map hf hφ.ae_eq_mk
have hψ_ae := ae_of_ae_map hg hψ.ae_eq_mk
refine IndepFun.congr' h ?_ ?_
· filter_upwards [Measure.ae_ae_of_ae_comp (hφ_ae)] with a haφ
filter_upwards [haφ] with ω hωφ
simp [hωφ]
· filter_upwards [Measure.ae_ae_of_ae_comp (hψ_ae)] with a haψ
filter_upwards [haψ] with ω hωψ
simp [hωψ]
