English
If X and Y are independent under μ and (X,Y) is identically distributed to (X',Y') under μ and μ', then X' and Y' are independent under μ'.
Русский
Если X и Y независимы по μ и (X,Y) равно по распределению (X',Y') по μ и μ', то X' и Y' независимы по μ'.
LaTeX
$$$IndepFun X Y μ \land IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ' \Rightarrow IndepFun X' Y' μ'$$
Lean4
/-- If `X` and `Y` are independent and `(X, Y)` and `(X', Y')` are identically distributed,
then `X'` and `Y'` are independent. -/
theorem indepFun_of_identDistrib_pair {μ : Measure γ} {μ' : Measure δ} [IsFiniteMeasure μ] [IsFiniteMeasure μ']
{X : γ → α} {X' : δ → α} {Y : γ → β} {Y' : δ → β} (h_indep : IndepFun X Y μ)
(h_ident : IdentDistrib (fun ω ↦ (X ω, Y ω)) (fun ω ↦ (X' ω, Y' ω)) μ μ') : IndepFun X' Y' μ' :=
by
rw [indepFun_iff_map_prod_eq_prod_map_map _ _, ← h_ident.map_eq,
(indepFun_iff_map_prod_eq_prod_map_map _ _).1 h_indep]
· exact congr (congrArg Measure.prod <| (h_ident.comp measurable_fst).map_eq) (h_ident.comp measurable_snd).map_eq
· exact measurable_fst.aemeasurable.comp_aemeasurable h_ident.aemeasurable_fst
· exact measurable_snd.aemeasurable.comp_aemeasurable h_ident.aemeasurable_fst
· exact measurable_fst.aemeasurable.comp_aemeasurable h_ident.aemeasurable_snd
· exact measurable_snd.aemeasurable.comp_aemeasurable h_ident.aemeasurable_snd
