Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
⊢ Indep (⨆ (i : ι), m i) m'
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
⊢ Indep (⨆ (i : ι), m i) m'
let p : ι → Set (Set Ω) := fun n => { t | MeasurableSet[m n] t }
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
⊢ Indep (⨆ (i : ι), m i) m'
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
⊢ Indep (⨆ (i : ι), m i) m'
have hp : ∀ n, IsPiSystem (p n) := fun n => @isPiSystem_measurableSet Ω (m n)
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
⊢ Indep (⨆ (i : ι), m i) m'
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
⊢ Indep (⨆ (i : ι), m i) m'
have h_gen_n : ∀ n, m n = generateFrom (p n) := fun n =>
  (@generateFrom_measurableSet Ω (m n)).symm
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ (n : ι), p n)
⊢ Indep (⨆ (i : ι), m i) m'
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
⊢ Indep (⨆ (i : ι), m i) m'
have hp_supr_pi : IsPiSystem (⋃ n, p n) := isPiSystem_iUnion_of_directed_le p hp hm
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
⊢ Indep (⨆ (i : ι), m i) m'
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ (n : ι), p n)
⊢ Indep (⨆ (i : ι), m i) m'
let p' := { t : Set Ω | MeasurableSet[m'] t }
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
⊢ Indep (⨆ (i : ι), m i) m'
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
⊢ Indep (⨆ (i : ι), m i) m'
have hp'_pi : IsPiSystem p' := @isPiSystem_measurableSet Ω m'
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ Indep (⨆ (i : ι), m i) m'
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
⊢ Indep (⨆ (i : ι), m i) m'
have h_gen' : m' = generateFrom p' := (@generateFrom_measurableSet Ω m').symm
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
h_pi_system_indep : IndepSets (⋃ (n : ι), p n) p'
⊢ Indep (⨆ (i : ι), m i) m'
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ Indep (⨆ (i : ι), m i) m'
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
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
h_pi_system_indep : IndepSets (⋃ (n : ι), p n) p'
⊢ (⨆ (i : ι), m i) = generateFrom (⋃ (n : ι), p n)
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
h_pi_system_indep : IndepSets (⋃ (n : ι), p n) p'
⊢ Indep (⨆ (i : ι), m i) m'
refine' IndepSets.indep (iSup_le h_le) h_le' hp_supr_pi hp'_pi _ h_gen' h_pi_system_indep
no goals
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
h_pi_system_indep : IndepSets (⋃ (n : ι), p n) p'
⊢ (⨆ (i : ι), m i) = generateFrom (⋃ (n : ι), p n)
exact (generateFrom_iUnion_measurableSet _).symm
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ ∀ (n : ι), IndepSets (p n) p'
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ IndepSets (⋃ (n : ι), p n) p'
refine IndepSets.iUnion ?_
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
h_indep : ∀ (i : ι), Indep (generateFrom (p i)) (generateFrom p')
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ ∀ (n : ι), IndepSets (p n) p'
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m'
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ ∀ (n : ι), IndepSets (p n) p'
conv at h_indep =>
  intro i
  rw [h_gen_n i, h_gen']
no goals
Ω✝ : Type ?u.2077013
ι : Type u_2
m0✝ : MeasurableSpace Ω✝
μ✝ : MeasureTheory.Measure Ω✝
Ω : Type u_1
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x x_1 => x ≤ x_1) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
h_indep : ∀ (i : ι), Indep (generateFrom (p i)) (generateFrom p')
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ ∀ (n : ι), IndepSets (p n) p'
exact fun n => (h_indep n).indepSets