Lean4
/-- If `f` is a family of mutually independent random variables (`iIndepFun m f μ`) and `S, T` are
two disjoint finite index sets, then the tuple formed by `f i` for `i ∈ S` is independent of the
tuple `(f i)_i` for `i ∈ T`. -/
theorem indepFun_finset (S T : Finset ι) (hST : Disjoint S T) (hf_Indep : iIndepFun f κ μ)
(hf_meas : ∀ i, Measurable (f i)) : IndepFun (fun a (i : S) => f i a) (fun a (i : T) => f i a) κ μ :=
by
rcases eq_or_ne μ 0 with rfl | hμ
· simp
obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
exists_ae_eq_isMarkovKernel hf_Indep.ae_isProbabilityMeasure hμ
apply
IndepFun.congr
(Filter.EventuallyEq.symm η_eq)
-- We introduce π-systems, built from the π-system of boxes which generates `MeasurableSpace.pi`.
let πSβ := Set.pi (Set.univ : Set S) '' Set.pi (Set.univ : Set S) fun i => {s : Set (β i) | MeasurableSet[m i] s}
let πS := {s : Set Ω | ∃ t ∈ πSβ, (fun a (i : S) => f i a) ⁻¹' t = s}
have hπS_pi : IsPiSystem πS := by exact IsPiSystem.comap (@isPiSystem_pi _ _ ?_) _
have hπS_gen : (MeasurableSpace.pi.comap fun a (i : S) => f i a) = generateFrom πS :=
by
rw [generateFrom_pi.symm, comap_generateFrom]
congr
let πTβ := Set.pi (Set.univ : Set T) '' Set.pi (Set.univ : Set T) fun i => {s : Set (β i) | MeasurableSet[m i] s}
let πT := {s : Set Ω | ∃ t ∈ πTβ, (fun a (i : T) => f i a) ⁻¹' t = s}
have hπT_pi : IsPiSystem πT := by exact IsPiSystem.comap (@isPiSystem_pi _ _ ?_) _
have hπT_gen : (MeasurableSpace.pi.comap fun a (i : T) => f i a) = generateFrom πT :=
by
rw [generateFrom_pi.symm, comap_generateFrom]
congr
-- To prove independence, we prove independence of the generating π-systems.
refine
IndepSets.indep (Measurable.comap_le (measurable_pi_iff.mpr fun i => hf_meas i))
(Measurable.comap_le (measurable_pi_iff.mpr fun i => hf_meas i)) hπS_pi hπT_pi hπS_gen hπT_gen ?_
rintro _ _ ⟨s, ⟨sets_s, hs1, hs2⟩, rfl⟩ ⟨t, ⟨sets_t, ht1, ht2⟩, rfl⟩
simp only [Set.mem_univ_pi, Set.mem_setOf_eq] at hs1 ht1
rw [← hs2, ← ht2]
classical
let sets_s' : ∀ i : ι, Set (β i) := fun i => dite (i ∈ S) (fun hi => sets_s ⟨i, hi⟩) fun _ => Set.univ
have h_sets_s'_eq : ∀ {i} (hi : i ∈ S), sets_s' i = sets_s ⟨i, hi⟩ := by intro i hi; simp_rw [sets_s', dif_pos hi]
have h_sets_s'_univ : ∀ {i} (_hi : i ∈ T), sets_s' i = Set.univ := by intro i hi;
simp_rw [sets_s', dif_neg (Finset.disjoint_right.mp hST hi)]
let sets_t' : ∀ i : ι, Set (β i) := fun i => dite (i ∈ T) (fun hi => sets_t ⟨i, hi⟩) fun _ => Set.univ
have h_sets_t'_univ : ∀ {i} (_hi : i ∈ S), sets_t' i = Set.univ := by intro i hi;
simp_rw [sets_t', dif_neg (Finset.disjoint_left.mp hST hi)]
have h_meas_s' : ∀ i ∈ S, MeasurableSet (sets_s' i) := by intro i hi; rw [h_sets_s'_eq hi]; exact hs1 _
have h_meas_t' : ∀ i ∈ T, MeasurableSet (sets_t' i) := by intro i hi; simp_rw [sets_t', dif_pos hi]; exact ht1 _
have h_eq_inter_S : (fun (ω : Ω) (i : ↥S) => f (↑i) ω) ⁻¹' Set.pi Set.univ sets_s = ⋂ i ∈ S, f i ⁻¹' sets_s' i :=
by
ext1 x
simp_rw [Set.mem_preimage, Set.mem_univ_pi, Set.mem_iInter]
grind
have h_eq_inter_T : (fun (ω : Ω) (i : ↥T) => f (↑i) ω) ⁻¹' Set.pi Set.univ sets_t = ⋂ i ∈ T, f i ⁻¹' sets_t' i :=
by
ext1 x
simp only [Set.mem_preimage, Set.mem_univ_pi, Set.mem_iInter]
constructor <;> intro h
· intro i hi; simp_rw [sets_t', dif_pos hi]; exact h ⟨i, hi⟩
· grind
replace hf_Indep := hf_Indep.congr η_eq
rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at hf_Indep
have h_Inter_inter :
((⋂ i ∈ S, f i ⁻¹' sets_s' i) ∩ ⋂ i ∈ T, f i ⁻¹' sets_t' i) = ⋂ i ∈ S ∪ T, f i ⁻¹' (sets_s' i ∩ sets_t' i) :=
by
ext1 x
simp_rw [Set.mem_inter_iff, Set.mem_iInter, Set.mem_preimage, Finset.mem_union]
constructor <;> intro h
· grind
· exact ⟨fun i hi => (h i (Or.inl hi)).1, fun i hi => (h i (Or.inr hi)).2⟩
have h_meas_inter : ∀ i ∈ S ∪ T, MeasurableSet (sets_s' i ∩ sets_t' i) :=
by
intro i hi_mem
rw [Finset.mem_union] at hi_mem
rcases hi_mem with hi_mem | hi_mem
· rw [h_sets_t'_univ hi_mem, Set.inter_univ]
exact h_meas_s' i hi_mem
· rw [h_sets_s'_univ hi_mem, Set.univ_inter]
exact h_meas_t' i hi_mem
filter_upwards [hf_Indep S h_meas_s', hf_Indep T h_meas_t', hf_Indep (S ∪ T) h_meas_inter] with a h_indepS h_indepT
h_indepST
rw [h_eq_inter_S, h_eq_inter_T, h_indepS, h_indepT, h_Inter_inter, h_indepST, Finset.prod_union hST]
congr 1
· refine Finset.prod_congr rfl fun i hi => ?_
rw [h_sets_t'_univ hi, Set.inter_univ]
· refine Finset.prod_congr rfl fun i hi => ?_
rw [h_sets_s'_univ hi, Set.univ_inter]
