-- Mathlib/Probability/IdentDistrib.lean
/-- If `X` and `Y` are independent and `(X, Y)` and `(X', Y')` are identically distributed,
then `X'` and `Y'` are independent. -/
lemma 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' μ'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : IndepFun X Y μ
h_ident : IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ'
⊢ AEMeasurable X μ

Tactic:
exact measurable_fst.aemeasurable.comp_aemeasurable h_ident.aemeasurable_fst

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : IndepFun X Y μ
h_ident : IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ'
⊢ AEMeasurable Y' μ'

Tactic:
exact measurable_snd.aemeasurable.comp_aemeasurable h_ident.aemeasurable_snd

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : IndepFun X Y μ
h_ident : IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ'
⊢ AEMeasurable X' μ'

Tactic:
exact measurable_fst.aemeasurable.comp_aemeasurable h_ident.aemeasurable_snd

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : IndepFun X Y μ
h_ident : IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ'
⊢ IndepFun X' Y' μ'

Tactic:
rw [indepFun_iff_map_prod_eq_prod_map_map _ _, ← h_ident.map_eq,
  (indepFun_iff_map_prod_eq_prod_map_map _ _).1 h_indep]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : IndepFun X Y μ
h_ident : IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ'
⊢ (Measure.map X μ).prod (Measure.map Y μ) = (Measure.map X' μ').prod (Measure.map Y' μ')

α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : IndepFun X Y μ
h_ident : IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ'
⊢ AEMeasurable X μ

α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : IndepFun X Y μ
h_ident : IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ'
⊢ AEMeasurable Y μ

α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : IndepFun X Y μ
h_ident : IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ'
⊢ AEMeasurable X' μ'

α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : IndepFun X Y μ
h_ident : IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ'
⊢ AEMeasurable Y' μ'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : IndepFun X Y μ
h_ident : IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ'
⊢ AEMeasurable Y μ

Tactic:
exact measurable_snd.aemeasurable.comp_aemeasurable h_ident.aemeasurable_fst

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure γ
μ' : Measure δ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
X : γ → α
X' : δ → α
Y : γ → β
Y' : δ → β
h_indep : IndepFun X Y μ
h_ident : IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ'
⊢ (Measure.map X μ).prod (Measure.map Y μ) = (Measure.map X' μ').prod (Measure.map Y' μ')

Tactic:
exact congr (congrArg Measure.prod <| (h_ident.comp measurable_fst).map_eq)
  (h_ident.comp measurable_snd).map_eq

Result:
no goals