case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
⊢ ∀ (i : α), Indep (⨆ (n : ι) (_ : n ∈ ns i), s n) (limsup s f)

case refine'_2
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
⊢ ∀ (i : α), (⨆ (n : ι) (_ : n ∈ ns i), s n) ≤ m0

case refine'_3
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
⊢ limsup s f ≤ m0

case refine'_4
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
⊢ Directed (fun x x_1 => x ≤ x_1) fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
⊢ Indep (⨆ (a : α) (n : ι) (_ : n ∈ ns a), s n) (limsup s f)
refine' indep_iSup_of_directed_le _ _ _ _
no goals
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
⊢ ∀ (i : α), Indep (⨆ (n : ι) (_ : n ∈ ns i), s n) (limsup s f)
exact fun a => indep_biSup_limsup h_le h_indep hf (hnsp a)
no goals
case refine'_2
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
⊢ ∀ (i : α), (⨆ (n : ι) (_ : n ∈ ns i), s n) ≤ m0
exact fun a => iSup₂_le fun n _ => h_le n
no goals
case refine'_3
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
⊢ limsup s f ≤ m0
exact limsup_le_iSup.trans (iSup_le h_le)
case refine'_4
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
a b : α
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) a) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) z) ∧
      (fun x x_1 => x ≤ x_1) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) b) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) z)
case refine'_4
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
⊢ Directed (fun x x_1 => x ≤ x_1) fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n
intro a b
case refine'_4.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
a b c : α
hc : (fun x x_1 => x ≤ x_1) (ns a) (ns c) ∧ (fun x x_1 => x ≤ x_1) (ns b) (ns c)
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) a) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) z) ∧
      (fun x x_1 => x ≤ x_1) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) b) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) z)
case refine'_4
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
a b : α
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) a) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) z) ∧
      (fun x x_1 => x ≤ x_1) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) b) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) z)
obtain ⟨c, hc⟩ := hns a b
case refine'_4.intro.refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
a b c : α
hc : (fun x x_1 => x ≤ x_1) (ns a) (ns c) ∧ (fun x x_1 => x ≤ x_1) (ns b) (ns c)
n : ι
hn : n ∈ ns a
⊢ n ∈ ns c

case refine'_4.intro.refine'_2
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
a b c : α
hc : (fun x x_1 => x ≤ x_1) (ns a) (ns c) ∧ (fun x x_1 => x ≤ x_1) (ns b) (ns c)
n : ι
hn : n ∈ ns b
⊢ n ∈ ns c
case refine'_4.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
a b c : α
hc : (fun x x_1 => x ≤ x_1) (ns a) (ns c) ∧ (fun x x_1 => x ≤ x_1) (ns b) (ns c)
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) a) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) z) ∧
      (fun x x_1 => x ≤ x_1) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) b) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) z)
refine' ⟨c, _, _⟩ <;> refine' iSup_mono fun n => iSup_mono' fun hn => ⟨_, le_rfl⟩
no goals
case refine'_4.intro.refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
a b c : α
hc : (fun x x_1 => x ≤ x_1) (ns a) (ns c) ∧ (fun x x_1 => x ≤ x_1) (ns b) (ns c)
n : ι
hn : n ∈ ns a
⊢ n ∈ ns c
exact hc.1 hn
no goals
case refine'_4.intro.refine'_2
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
a b c : α
hc : (fun x x_1 => x ≤ x_1) (ns a) (ns c) ∧ (fun x x_1 => x ≤ x_1) (ns b) (ns c)
n : ι
hn : n ∈ ns b
⊢ n ∈ ns c
exact hc.2 hn