English
Under directedness and measurability, independence passes to iSup of the left-right sigma-algebras.
Русский
При направленности и измеримости независимость переходит к iSup левых и правых сигма-алгебр.
LaTeX
$$indep_iSup_of_directed_le {m : ι → MeasurableSpace Ω} (h_indep : ∀ i, Indep (m i) m' κ μ) (h_le : ∀ i, m i ≤ m0) (h_le' : m' ≤ m0) (hm : Directed (· ≤ ·) m) : Indep (iSup fun i => m i) m' κ μ$$
Lean4
theorem indep_iSup_of_disjoint {m : ι → MeasurableSpace Ω} (h_le : ∀ i, m i ≤ _mΩ) (h_indep : iIndep m κ μ)
{S T : Set ι} (hST : Disjoint S T) : Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ := by
classical
rcases eq_or_ne μ 0 with rfl | hμ
· simp
obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
exists_ae_eq_isMarkovKernel h_indep.ae_isProbabilityMeasure hμ
apply Indep.congr (Filter.EventuallyEq.symm η_eq)
refine
IndepSets.indep (iSup₂_le fun i _ => h_le i) (iSup₂_le fun i _ => h_le i) ?_ ?_
(generateFrom_piiUnionInter_measurableSet m S).symm (generateFrom_piiUnionInter_measurableSet m T).symm ?_
· exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _
· exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _
· exact indepSets_piiUnionInter_of_disjoint (h_indep.congr η_eq) hST
