English
If f_i are functions and g_i are measurable, then the composition of iIndepFun with g_i preserves independence structure.
Русский
Если f_i — функции, a g_i — измеримы, то композиция iIndepFun с g_i сохраняет структуру независимости.
LaTeX
$$$iIndepFun f κ μ \Rightarrow iIndepFun (i \mapsto g_i \circ f_i) κ μ$$$
Lean4
theorem comp₀ {β γ : ι → Type*} {mβ : ∀ i, MeasurableSpace (β i)} {mγ : ∀ i, MeasurableSpace (γ i)} {f : ∀ i, Ω → β i}
(h : iIndepFun f κ μ) (g : ∀ i, β i → γ i) (hf : ∀ i, AEMeasurable (f i) (κ ∘ₘ μ))
(hg : ∀ i, AEMeasurable (g i) ((κ ∘ₘ μ).map (f i))) : iIndepFun (fun i ↦ g i ∘ f i) κ μ :=
by
have h : iIndepFun (fun i ↦ ((hg i).mk (g i)) ∘ f i) κ μ :=
iIndepFun.comp h (fun i ↦ (hg i).mk (g i)) fun i ↦ (hg i).measurable_mk
have h_ae i := ae_of_ae_map (hf i) (hg i).ae_eq_mk.symm
exact iIndepFun.congr' h fun i ↦ Measure.ae_ae_of_ae_comp (h_ae i)
