English
The measurable-space structures generated by independent pi-systems are themselves independent. If each m_i ≤ mΩ and m_i = generateFrom(π_i), and the π_i are pi-systems and are independent, then the resulting family m_i is independent.
Русский
Структуры сигма-алгебр, порожденные независимыми пи-системами, сами являются независимыми. Если m_i ≤ mΩ и m_i = generateFrom(π_i), и π_i — пи-системы, независимые между собой, то соответствующая семья m_i независима.
LaTeX
$$$Indep\left(m_i\right)\ κ\ μ$ where $m_i = \ generateFrom(\pi_i)$ and independence of the π_i holds.$$
Lean4
/-- The measurable space structures generated by independent pi-systems are independent. -/
theorem iIndep (m : ι → MeasurableSpace Ω) (h_le : ∀ i, m i ≤ _mΩ) (π : ι → Set (Set Ω)) (h_pi : ∀ n, IsPiSystem (π n))
(h_generate : ∀ i, m i = generateFrom (π i)) (h_ind : iIndepSets π κ μ) : iIndep m κ μ := by
classical
rcases eq_or_ne μ 0 with rfl | hμ
· simp
obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
exists_ae_eq_isMarkovKernel h_ind.ae_isProbabilityMeasure hμ
apply iIndep.congr (Filter.EventuallyEq.symm η_eq)
intro s f
refine Finset.induction ?_ ?_ s
·
simp only [Finset.notMem_empty, Set.mem_setOf_eq, IsEmpty.forall_iff, implies_true, Set.iInter_of_empty,
Set.iInter_univ, measure_univ, Finset.prod_empty, Filter.eventually_true]
· intro a S ha_notin_S h_rec hf_m
have hf_m_S : ∀ x ∈ S, MeasurableSet[m x] (f x) := fun x hx => hf_m x (by simp [hx])
let p := piiUnionInter π S
set m_p := generateFrom p with hS_eq_generate
have h_indep : Indep m_p (m a) η μ :=
by
have hp : IsPiSystem p := isPiSystem_piiUnionInter π h_pi S
have h_le' : ∀ i, generateFrom (π i) ≤ _mΩ := fun i ↦ (h_generate i).symm.trans_le (h_le i)
have hm_p : m_p ≤ _mΩ := generateFrom_piiUnionInter_le π h_le' S
exact
IndepSets.indep hm_p (h_le a) hp (h_pi a) hS_eq_generate (h_generate a)
(iIndepSets.piiUnionInter_of_notMem (h_ind.congr η_eq) ha_notin_S)
have h := h_indep.symm (f a) (⋂ n ∈ S, f n) (hf_m a (Finset.mem_insert_self a S)) ?_
· filter_upwards [h_rec hf_m_S, h] with a' ha' h'
rwa [Finset.set_biInter_insert, Finset.prod_insert ha_notin_S, ← ha']
· have h_le_p : ∀ i ∈ S, m i ≤ m_p := by
intro n hn
rw [hS_eq_generate, h_generate n]
exact le_generateFrom_piiUnionInter (S : Set ι) hn
have h_S_f : ∀ i ∈ S, MeasurableSet[m_p] (f i) := fun i hi ↦ (h_le_p i hi) (f i) (hf_m_S i hi)
exact S.measurableSet_biInter h_S_f
