English
A variant formulation of indep_iSup_of_directed_le with similar hypotheses.
Русский
Вариант формулировки indep_iSup_of_directed_le с похожими предпосылками.
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_directed_le {Ω} {m : ι → MeasurableSpace Ω} {m' m0 : MeasurableSpace Ω} {κ : Kernel α Ω}
{μ : Measure α} [IsZeroOrMarkovKernel κ] (h_indep : ∀ i, Indep (m i) m' κ μ) (h_le : ∀ i, m i ≤ m0)
(h_le' : m' ≤ m0) (hm : Directed (· ≤ ·) m) : Indep (⨆ i, m i) m' κ μ :=
by
let p : ι → Set (Set Ω) := fun n => {t | MeasurableSet[m n] t}
have hp : ∀ n, IsPiSystem (p n) := fun n => @isPiSystem_measurableSet Ω (m n)
have h_gen_n : ∀ n, m n = generateFrom (p n) := fun n => (@generateFrom_measurableSet Ω (m n)).symm
have hp_supr_pi : IsPiSystem (⋃ n, p n) := isPiSystem_iUnion_of_directed_le p hp hm
let p' := {t : Set Ω | MeasurableSet[m'] t}
have hp'_pi : IsPiSystem p' := @isPiSystem_measurableSet Ω m'
have h_gen' : m' = generateFrom p' := (@generateFrom_measurableSet Ω m').symm
have h_pi_system_indep : IndepSets (⋃ n, p n) p' κ μ :=
by
refine IndepSets.iUnion ?_
conv at h_indep =>
intro i
rw [h_gen_n i, h_gen']
exact fun n => (h_indep n).indepSets
refine IndepSets.indep (iSup_le h_le) h_le' hp_supr_pi hp'_pi ?_ h_gen' h_pi_system_indep
exact (generateFrom_iUnion_measurableSet _).symm
