English
If a family of sigma-algebras m_i is directed and independent with respect to κ and μ, then the iSup over disjoint index sets is independent.
Русский
Если семейство сигма-алгебр {m_i} упорядочиваемо и независимо, то iSup по дискретным подмножествам индексов сохраняет независимость.
LaTeX
$$Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ$$
Lean4
theorem indepSets_piiUnionInter_of_disjoint {s : ι → Set (Set Ω)} {S T : Set ι} (h_indep : iIndepSets s κ μ)
(hST : Disjoint S T) : IndepSets (piiUnionInter s S) (piiUnionInter s T) κ μ :=
by
rintro t1 t2 ⟨p1, hp1, f1, ht1_m, ht1_eq⟩ ⟨p2, hp2, f2, ht2_m, ht2_eq⟩
classical
let g i := ite (i ∈ p1) (f1 i) Set.univ ∩ ite (i ∈ p2) (f2 i) Set.univ
have h_P_inter : ∀ᵐ a ∂μ, κ a (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, κ a (g n) :=
by
have hgm : ∀ i ∈ p1 ∪ p2, g i ∈ s i := by
intro i hi_mem_union
rw [Finset.mem_union] at hi_mem_union
rcases hi_mem_union with hi1 | hi2
· have hi2 : i ∉ p2 := fun hip2 => Set.disjoint_left.mp hST (hp1 hi1) (hp2 hip2)
simp_rw [g, if_pos hi1, if_neg hi2, Set.inter_univ]
exact ht1_m i hi1
· have hi1 : i ∉ p1 := fun hip1 => Set.disjoint_right.mp hST (hp2 hi2) (hp1 hip1)
simp_rw [g, if_neg hi1, if_pos hi2, Set.univ_inter]
exact ht2_m i hi2
have h_p1_inter_p2 :
((⋂ x ∈ p1, f1 x) ∩ ⋂ x ∈ p2, f2 x) =
⋂ i ∈ p1 ∪ p2, ite (i ∈ p1) (f1 i) Set.univ ∩ ite (i ∈ p2) (f2 i) Set.univ :=
by
ext1 x
simp only [Set.mem_ite_univ_right, Set.mem_inter_iff, Set.mem_iInter, Finset.mem_union]
exact
⟨fun h i _ => ⟨h.1 i, h.2 i⟩, fun h => ⟨fun i hi => (h i (Or.inl hi)).1 hi, fun i hi => (h i (Or.inr hi)).2 hi⟩⟩
filter_upwards [h_indep _ hgm] with a ha
rw [ht1_eq, ht2_eq, h_p1_inter_p2, ← ha]
filter_upwards [h_P_inter, h_indep p1 ht1_m, h_indep p2 ht2_m, h_indep.ae_isProbabilityMeasure] with a h_P_inter ha1
ha2 h'
have h_μg : ∀ n, κ a (g n) = (ite (n ∈ p1) (κ a (f1 n)) 1) * (ite (n ∈ p2) (κ a (f2 n)) 1) :=
by
intro n
dsimp only [g]
split_ifs with h1 h2
· exact absurd rfl (Set.disjoint_iff_forall_ne.mp hST (hp1 h1) (hp2 h2))
all_goals simp only [measure_univ, one_mul, mul_one, Set.inter_univ, Set.univ_inter]
simp_rw [h_P_inter, h_μg, Finset.prod_mul_distrib, Finset.prod_ite_mem (p1 ∪ p2) p1 (fun x ↦ κ a (f1 x)),
Finset.union_inter_cancel_left, Finset.prod_ite_mem (p1 ∪ p2) p2 (fun x => κ a (f2 x)),
Finset.union_inter_cancel_right, ht1_eq, ← ha1, ht2_eq, ← ha2]
