[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
t : Set Ω
h_indep : IndepSet t t
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
[PROOFSTEP]
rw [IndepSet_iff] at h_indep 
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
t : Set Ω
h_indep : ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
[PROOFSTEP]
specialize
  h_indep t t (measurableSet_generateFrom (Set.mem_singleton t)) (measurableSet_generateFrom (Set.mem_singleton t))
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
[PROOFSTEP]
by_cases h0 : μ t = 0
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
h0 : ↑↑μ t = 0
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
[PROOFSTEP]
exact Or.inl h0
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
h0 : ¬↑↑μ t = 0
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
[PROOFSTEP]
by_cases h_top : μ t = ∞
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
h0 : ¬↑↑μ t = 0
h_top : ↑↑μ t = ⊤
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
[PROOFSTEP]
exact Or.inr (Or.inr h_top)
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
h0 : ¬↑↑μ t = 0
h_top : ¬↑↑μ t = ⊤
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
[PROOFSTEP]
rw [← one_mul (μ (t ∩ t)), Set.inter_self, ENNReal.mul_eq_mul_right h0 h_top] at h_indep 
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
t : Set Ω
h_indep : 1 = ↑↑μ t
h0 : ¬↑↑μ t = 0
h_top : ¬↑↑μ t = ⊤
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
[PROOFSTEP]
exact Or.inr (Or.inl h_indep.symm)
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
t : Set Ω
h_indep : IndepSet t t
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1
[PROOFSTEP]
have h_0_1_top := measure_eq_zero_or_one_or_top_of_indepSet_self h_indep
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
t : Set Ω
h_indep : IndepSet t t
h_0_1_top : ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1
[PROOFSTEP]
simpa [measure_ne_top μ] using h_0_1_top
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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
t : Set ι
ht : p t
⊢ Indep (⨆ (n : ι) (_ : n ∈ t), s n) (limsup s f)
[PROOFSTEP]
refine' indep_of_indep_of_le_right (indep_biSup_compl h_le h_indep t) _
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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
t : Set ι
ht : p t
⊢ limsup s f ≤ ⨆ (n : ι) (_ : n ∈ tᶜ), s n
[PROOFSTEP]
refine' limsSup_le_of_le (by isBoundedDefault) _
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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
t : Set ι
ht : p t
⊢ IsCobounded (fun x x_1 => x ≤ x_1) (map s f)
[PROOFSTEP]
isBoundedDefault
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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
t : Set ι
ht : p t
⊢ ∀ᶠ (n : MeasurableSpace Ω) in map s f, n ≤ ⨆ (n : ι) (_ : n ∈ tᶜ), s n
[PROOFSTEP]
simp only [Set.mem_compl_iff, eventually_map]
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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
t : Set ι
ht : p t
⊢ ∀ᶠ (a : ι) in f, s a ≤ ⨆ (n : ι) (_ : ¬n ∈ t), s n
[PROOFSTEP]
exact eventually_of_mem (hf t ht) le_iSup₂
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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)
[PROOFSTEP]
refine' indep_iSup_of_directed_le _ _ _ _
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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)
[PROOFSTEP]
exact fun a => indep_biSup_limsup h_le h_indep hf (hnsp a)
[GOAL]
case refine'_2
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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
[PROOFSTEP]
exact fun a => iSup₂_le fun n _ => h_le n
[GOAL]
case refine'_3
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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
[PROOFSTEP]
exact limsup_le_iSup.trans (iSup_le h_le)
[GOAL]
case refine'_4
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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
[PROOFSTEP]
intro a b
[GOAL]
case refine'_4
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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)
[PROOFSTEP]
obtain ⟨c, hc⟩ := hns a b
[GOAL]
case refine'_4.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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)
[PROOFSTEP]
refine' ⟨c, _, _⟩
[GOAL]
case refine'_4.intro.refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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)
⊢ (fun x x_1 => x ≤ x_1) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) a) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) c)
[PROOFSTEP]
refine' iSup_mono fun n => iSup_mono' fun hn => ⟨_, le_rfl⟩
[GOAL]
case refine'_4.intro.refine'_2
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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)
⊢ (fun x x_1 => x ≤ x_1) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) b) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) c)
[PROOFSTEP]
refine' iSup_mono fun n => iSup_mono' fun hn => ⟨_, le_rfl⟩
[GOAL]
case refine'_4.intro.refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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
[PROOFSTEP]
exact hc.1 hn
[GOAL]
case refine'_4.intro.refine'_2
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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
[PROOFSTEP]
exact hc.2 hn
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
⊢ Indep (⨆ (n : ι), s n) (limsup s f)
[PROOFSTEP]
suffices (⨆ a, ⨆ n ∈ ns a, s n) = ⨆ n, s n by
  rw [← this]
  exact indep_iSup_directed_limsup h_le h_indep hf hns hnsp
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
this : ⨆ (a : α) (n : ι) (_ : n ∈ ns a), s n = ⨆ (n : ι), s n
⊢ Indep (⨆ (n : ι), s n) (limsup s f)
[PROOFSTEP]
rw [← this]
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
this : ⨆ (a : α) (n : ι) (_ : n ∈ ns a), s n = ⨆ (n : ι), s n
⊢ Indep (⨆ (a : α) (n : ι) (_ : n ∈ ns a), s n) (limsup s f)
[PROOFSTEP]
exact indep_iSup_directed_limsup h_le h_indep hf hns hnsp
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
⊢ ⨆ (a : α) (n : ι) (_ : n ∈ ns a), s n = ⨆ (n : ι), s n
[PROOFSTEP]
rw [iSup_comm]
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
⊢ ⨆ (j : ι) (i : α) (_ : j ∈ ns i), s j = ⨆ (n : ι), s n
[PROOFSTEP]
refine' iSup_congr fun n => _
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
n : ι
⊢ ⨆ (i : α) (_ : n ∈ ns i), s n = s n
[PROOFSTEP]
have h : ⨆ (i : α) (_ : n ∈ ns i), s n = ⨆ _ : ∃ i, n ∈ ns i, s n := by rw [iSup_exists]
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
n : ι
⊢ ⨆ (i : α) (_ : n ∈ ns i), s n = ⨆ (_ : ∃ i, n ∈ ns i), s n
[PROOFSTEP]
rw [iSup_exists]
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
n : ι
h : ⨆ (i : α) (_ : n ∈ ns i), s n = ⨆ (_ : ∃ i, n ∈ ns i), s n
⊢ ⨆ (i : α) (_ : n ∈ ns i), s n = s n
[PROOFSTEP]
haveI : Nonempty (∃ i : α, n ∈ ns i) := ⟨hns_univ n⟩
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : 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)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
n : ι
h : ⨆ (i : α) (_ : n ∈ ns i), s n = ⨆ (_ : ∃ i, n ∈ ns i), s n
this : Nonempty (∃ i, n ∈ ns i)
⊢ ⨆ (i : α) (_ : n ∈ ns i), s n = s n
[PROOFSTEP]
rw [h, iSup_const]
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
⊢ Indep (limsup s atTop) (limsup s atTop)
[PROOFSTEP]
let ns : ι → Set ι := Set.Iic
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
⊢ Indep (limsup s atTop) (limsup s atTop)
[PROOFSTEP]
have hnsp : ∀ i, BddAbove (ns i) := fun i => bddAbove_Iic
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ Indep (limsup s atTop) (limsup s atTop)
[PROOFSTEP]
refine' indep_limsup_self h_le h_indep _ _ hnsp _
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ ∀ (t : Set ι), BddAbove t → tᶜ ∈ atTop
[PROOFSTEP]
simp only [mem_atTop_sets, ge_iff_le, Set.mem_compl_iff, BddAbove, upperBounds, Set.Nonempty]
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ ∀ (t : Set ι), (∃ x, x ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}) → ∃ a, ∀ (b : ι), a ≤ b → ¬b ∈ t
[PROOFSTEP]
rintro t ⟨a, ha⟩
[GOAL]
case refine'_1.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
⊢ ∃ a, ∀ (b : ι), a ≤ b → ¬b ∈ t
[PROOFSTEP]
obtain ⟨b, hb⟩ : ∃ b, a < b := exists_gt a
[GOAL]
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
⊢ ∃ a, ∀ (b : ι), a ≤ b → ¬b ∈ t
[PROOFSTEP]
refine' ⟨b, fun c hc hct => _⟩
[GOAL]
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : b ≤ c
hct : c ∈ t
⊢ False
[PROOFSTEP]
suffices : ∀ i ∈ t, i < c
[GOAL]
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : b ≤ c
hct : c ∈ t
this : ∀ (i : ι), i ∈ t → i < c
⊢ False
case this
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : b ≤ c
hct : c ∈ t
⊢ ∀ (i : ι), i ∈ t → i < c
[PROOFSTEP]
exact lt_irrefl c (this c hct)
[GOAL]
case this
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : b ≤ c
hct : c ∈ t
⊢ ∀ (i : ι), i ∈ t → i < c
[PROOFSTEP]
exact fun i hi => (ha hi).trans_lt (hb.trans_le hc)
[GOAL]
case refine'_2
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ Directed (fun x x_1 => x ≤ x_1) fun a => ns a
[PROOFSTEP]
exact Monotone.directed_le fun i j hij k hki => le_trans hki hij
[GOAL]
case refine'_3
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ ∀ (n : ι), ∃ a, n ∈ ns a
[PROOFSTEP]
exact fun n => ⟨n, le_rfl⟩
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
⊢ Indep (limsup s atBot) (limsup s atBot)
[PROOFSTEP]
let ns : ι → Set ι := Set.Ici
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
⊢ Indep (limsup s atBot) (limsup s atBot)
[PROOFSTEP]
have hnsp : ∀ i, BddBelow (ns i) := fun i => bddBelow_Ici
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ Indep (limsup s atBot) (limsup s atBot)
[PROOFSTEP]
refine' indep_limsup_self h_le h_indep _ _ hnsp _
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (t : Set ι), BddBelow t → tᶜ ∈ atBot
[PROOFSTEP]
simp only [mem_atBot_sets, ge_iff_le, Set.mem_compl_iff, BddBelow, lowerBounds, Set.Nonempty]
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (t : Set ι), (∃ x, x ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}) → ∃ a, ∀ (b : ι), b ≤ a → ¬b ∈ t
[PROOFSTEP]
rintro t ⟨a, ha⟩
[GOAL]
case refine'_1.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
⊢ ∃ a, ∀ (b : ι), b ≤ a → ¬b ∈ t
[PROOFSTEP]
obtain ⟨b, hb⟩ : ∃ b, b < a := exists_lt a
[GOAL]
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
⊢ ∃ a, ∀ (b : ι), b ≤ a → ¬b ∈ t
[PROOFSTEP]
refine' ⟨b, fun c hc hct => _⟩
[GOAL]
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
⊢ False
[PROOFSTEP]
suffices : ∀ i ∈ t, c < i
[GOAL]
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
this : ∀ (i : ι), i ∈ t → c < i
⊢ False
case this
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
⊢ ∀ (i : ι), i ∈ t → c < i
[PROOFSTEP]
exact lt_irrefl c (this c hct)
[GOAL]
case this
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
⊢ ∀ (i : ι), i ∈ t → c < i
[PROOFSTEP]
exact fun i hi => hc.trans_lt (hb.trans_le (ha hi))
[GOAL]
case refine'_2
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ Directed (fun x x_1 => x ≤ x_1) fun a => ns a
[PROOFSTEP]
exact directed_of_inf fun i j hij k hki => hij.trans hki
[GOAL]
case refine'_3
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (n : ι), ∃ a, n ∈ ns a
[PROOFSTEP]
exact fun n => ⟨n, le_rfl⟩
