English
A variant statement asserting independence for iSup over disjoint indices under a collection directed by ≤.
Русский
Вариант утверждения независимости для iSup по дискретным индексам при направленном частично порядке.
LaTeX
$$indep_iSup_of_disjoint {m : ι → MeasurableSpace Ω} (h_le : ∀ i, m i ≤ _mΩ) (h_indep : iIndep m κ μ) (hST : Disjoint S T) : Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ$$
Lean4
theorem indep_generateFrom_of_disjoint {s : ι → Set Ω} (hsm : ∀ n, MeasurableSet (s n)) (hs : iIndepSet s κ μ)
(S T : Set ι) (hST : Disjoint S T) :
Indep (generateFrom {t | ∃ n ∈ S, s n = t}) (generateFrom {t | ∃ k ∈ T, s k = t}) κ μ := by
classical
rcases eq_or_ne μ 0 with rfl | hμ
· simp
obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
exists_ae_eq_isMarkovKernel hs.ae_isProbabilityMeasure hμ
apply Indep.congr (Filter.EventuallyEq.symm η_eq)
rw [← generateFrom_piiUnionInter_singleton_left, ← generateFrom_piiUnionInter_singleton_left]
refine
IndepSets.indep' (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht))
(fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht)) ?_ ?_ ?_
· exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k
· exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k
· exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _
· exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _
· exact indepSets_piiUnionInter_of_disjoint (iIndep.iIndepSets (fun n => rfl) (hs.congr η_eq)) hST
