[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f g : Filtration ι m
h : ↑f = ↑g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
g : Filtration ι m
seq✝ : ι → MeasurableSpace Ω
mono'✝ : Monotone seq✝
le'✝ : ∀ (i : ι), seq✝ i ≤ m
h : ↑{ seq := seq✝, mono' := mono'✝, le' := le'✝ } = ↑g
⊢ { seq := seq✝, mono' := mono'✝, le' := le'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
seq✝¹ : ι → MeasurableSpace Ω
mono'✝¹ : Monotone seq✝¹
le'✝¹ : ∀ (i : ι), seq✝¹ i ≤ m
seq✝ : ι → MeasurableSpace Ω
mono'✝ : Monotone seq✝
le'✝ : ∀ (i : ι), seq✝ i ≤ m
h : ↑{ seq := seq✝¹, mono' := mono'✝¹, le' := le'✝¹ } = ↑{ seq := seq✝, mono' := mono'✝, le' := le'✝ }
⊢ { seq := seq✝¹, mono' := mono'✝¹, le' := le'✝¹ } = { seq := seq✝, mono' := mono'✝, le' := le'✝ }
[PROOFSTEP]
congr
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
⊢ (fun i => sSup ((fun f => ↑f i) '' s)) i ≤ (fun i => sSup ((fun f => ↑f i) '' s)) j
[PROOFSTEP]
refine' sSup_le fun m' hm' => _
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
hm' : m' ∈ (fun f => ↑f i) '' s
⊢ m' ≤ (fun i => sSup ((fun f => ↑f i) '' s)) j
[PROOFSTEP]
rw [Set.mem_image] at hm' 
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
hm' : ∃ x, x ∈ s ∧ ↑x i = m'
⊢ m' ≤ (fun i => sSup ((fun f => ↑f i) '' s)) j
[PROOFSTEP]
obtain ⟨f, hf_mem, hfm'⟩ := hm'
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : ↑f i = m'
⊢ m' ≤ (fun i => sSup ((fun f => ↑f i) '' s)) j
[PROOFSTEP]
rw [← hfm']
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : ↑f i = m'
⊢ ↑f i ≤ (fun i => sSup ((fun f => ↑f i) '' s)) j
[PROOFSTEP]
refine' (f.mono hij).trans _
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : ↑f i = m'
⊢ ↑f j ≤ (fun i => sSup ((fun f => ↑f i) '' s)) j
[PROOFSTEP]
have hfj_mem : f j ∈ (fun g : Filtration ι m => g j) '' s := ⟨f, hf_mem, rfl⟩
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : ↑f i = m'
hfj_mem : ↑f j ∈ (fun g => ↑g j) '' s
⊢ ↑f j ≤ (fun i => sSup ((fun f => ↑f i) '' s)) j
[PROOFSTEP]
exact le_sSup hfj_mem
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
⊢ (fun i => sSup ((fun f => ↑f i) '' s)) i ≤ m
[PROOFSTEP]
refine' sSup_le fun m' hm' => _
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
hm' : m' ∈ (fun f => ↑f i) '' s
⊢ m' ≤ m
[PROOFSTEP]
rw [Set.mem_image] at hm' 
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
hm' : ∃ x, x ∈ s ∧ ↑x i = m'
⊢ m' ≤ m
[PROOFSTEP]
obtain ⟨f, _, hfm'⟩ := hm'
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
f : Filtration ι m
left✝ : f ∈ s
hfm' : ↑f i = m'
⊢ m' ≤ m
[PROOFSTEP]
rw [← hfm']
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
f : Filtration ι m
left✝ : f ∈ s
hfm' : ↑f i = m'
⊢ ↑f i ≤ m
[PROOFSTEP]
exact f.le i
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤
    (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) j
[PROOFSTEP]
by_cases h_nonempty : Set.Nonempty s
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : Set.Nonempty s
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤
    (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) j
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : ¬Set.Nonempty s
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤
    (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) j
[PROOFSTEP]
swap
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : ¬Set.Nonempty s
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤
    (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) j
[PROOFSTEP]
simp only [h_nonempty, Set.nonempty_image_iff, if_false, le_refl]
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : Set.Nonempty s
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤
    (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) j
[PROOFSTEP]
simp only [h_nonempty, if_true, le_sInf_iff, Set.mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : Set.Nonempty s
⊢ ∀ (a : Filtration ι m), a ∈ s → sInf ((fun f => ↑f i) '' s) ≤ ↑a j
[PROOFSTEP]
refine' fun f hf_mem => le_trans _ (f.mono hij)
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : Set.Nonempty s
f : Filtration ι m
hf_mem : f ∈ s
⊢ sInf ((fun f => ↑f i) '' s) ≤ ↑f i
[PROOFSTEP]
have hfi_mem : f i ∈ (fun g : Filtration ι m => g i) '' s := ⟨f, hf_mem, rfl⟩
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : Set.Nonempty s
f : Filtration ι m
hf_mem : f ∈ s
hfi_mem : ↑f i ∈ (fun g => ↑g i) '' s
⊢ sInf ((fun f => ↑f i) '' s) ≤ ↑f i
[PROOFSTEP]
exact sInf_le hfi_mem
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤ m
[PROOFSTEP]
by_cases h_nonempty : Set.Nonempty s
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : Set.Nonempty s
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤ m
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : ¬Set.Nonempty s
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤ m
[PROOFSTEP]
swap
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : ¬Set.Nonempty s
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤ m
[PROOFSTEP]
simp only [h_nonempty, if_false, le_refl]
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : Set.Nonempty s
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤ m
[PROOFSTEP]
simp only [h_nonempty, if_true]
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : Set.Nonempty s
⊢ sInf ((fun f => ↑f i) '' s) ≤ m
[PROOFSTEP]
obtain ⟨f, hf_mem⟩ := h_nonempty
[GOAL]
case pos.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
f : Filtration ι m
hf_mem : f ∈ s
⊢ sInf ((fun f => ↑f i) '' s) ≤ m
[PROOFSTEP]
exact le_trans (sInf_le ⟨f, hf_mem, rfl⟩) (f.le i)
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → b ≤ f
i : ι
m' : MeasurableSpace Ω
hm' : m' ∈ (fun f => ↑f i) '' s
⊢ m' ≤ ↑f i
[PROOFSTEP]
obtain ⟨g, hg_mem, hfm'⟩ := hm'
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → b ≤ f
i : ι
m' : MeasurableSpace Ω
g : Filtration ι m
hg_mem : g ∈ s
hfm' : (fun f => ↑f i) g = m'
⊢ m' ≤ ↑f i
[PROOFSTEP]
rw [← hfm']
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → b ≤ f
i : ι
m' : MeasurableSpace Ω
g : Filtration ι m
hg_mem : g ∈ s
hfm' : (fun f => ↑f i) g = m'
⊢ (fun f => ↑f i) g ≤ ↑f i
[PROOFSTEP]
exact h_forall g hg_mem i
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
hf_mem : f ∈ s
i : ι
⊢ ↑(sInf s) i ≤ ↑f i
[PROOFSTEP]
have hs : s.Nonempty := ⟨f, hf_mem⟩
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
hf_mem : f ∈ s
i : ι
hs : Set.Nonempty s
⊢ ↑(sInf s) i ≤ ↑f i
[PROOFSTEP]
simp only [sInf_def, hs, if_true]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
hf_mem : f ∈ s
i : ι
hs : Set.Nonempty s
⊢ sInf ((fun f => ↑f i) '' s) ≤ ↑f i
[PROOFSTEP]
exact sInf_le ⟨f, hf_mem, rfl⟩
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → f ≤ b
i : ι
⊢ ↑f i ≤ ↑(sInf s) i
[PROOFSTEP]
by_cases hs : s.Nonempty
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → f ≤ b
i : ι
hs : Set.Nonempty s
⊢ ↑f i ≤ ↑(sInf s) i
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → f ≤ b
i : ι
hs : ¬Set.Nonempty s
⊢ ↑f i ≤ ↑(sInf s) i
[PROOFSTEP]
swap
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → f ≤ b
i : ι
hs : ¬Set.Nonempty s
⊢ ↑f i ≤ ↑(sInf s) i
[PROOFSTEP]
simp only [sInf_def, hs, if_false]
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → f ≤ b
i : ι
hs : ¬Set.Nonempty s
⊢ ↑f i ≤ m
[PROOFSTEP]
exact f.le i
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → f ≤ b
i : ι
hs : Set.Nonempty s
⊢ ↑f i ≤ ↑(sInf s) i
[PROOFSTEP]
simp only [sInf_def, hs, if_true, le_sInf_iff, Set.mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → f ≤ b
i : ι
hs : Set.Nonempty s
⊢ ∀ (a : Filtration ι m), a ∈ s → ↑f i ≤ ↑a i
[PROOFSTEP]
exact fun g hg_mem => h_forall g hg_mem i
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
μ : Measure Ω
f : Filtration ι m
inst✝ : IsFiniteMeasure μ
n : ι
⊢ SigmaFinite (Measure.trim μ (_ : ↑f n ≤ m))
[PROOFSTEP]
infer_instance
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : TopologicalSpace β
inst✝² : MetrizableSpace β
mβ : MeasurableSpace β
inst✝¹ : BorelSpace β
inst✝ : Preorder ι
u : ι → Ω → β
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ (fun i => ⨆ (j : ι) (_ : j ≤ i), MeasurableSpace.comap (u j) mβ) i ≤ m
[PROOFSTEP]
refine' iSup₂_le _
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : TopologicalSpace β
inst✝² : MetrizableSpace β
mβ : MeasurableSpace β
inst✝¹ : BorelSpace β
inst✝ : Preorder ι
u : ι → Ω → β
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ ∀ (i_1 : ι), i_1 ≤ i → MeasurableSpace.comap (u i_1) mβ ≤ m
[PROOFSTEP]
rintro j _ s ⟨t, ht, rfl⟩
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : TopologicalSpace β
inst✝² : MetrizableSpace β
mβ : MeasurableSpace β
inst✝¹ : BorelSpace β
inst✝ : Preorder ι
u : ι → Ω → β
hum : ∀ (i : ι), StronglyMeasurable (u i)
i j : ι
j✝ : j ≤ i
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (u j ⁻¹' t)
[PROOFSTEP]
exact (hum j).measurable ht
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
⊢ filtrationOfSet hsm =
    natural (fun i => Set.indicator (s i) fun x => 1) (_ : ∀ (i : ι), StronglyMeasurable (Set.indicator (s i) 1))
[PROOFSTEP]
simp [natural, filtrationOfSet, measurableSpace_iSup_eq]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
⊢ (fun i => MeasurableSpace.generateFrom {t | ∃ j, j ≤ i ∧ s j = t}) = fun i =>
    MeasurableSpace.generateFrom {s_1 | ∃ n, MeasurableSet s_1}
[PROOFSTEP]
ext1 i
[GOAL]
case h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
⊢ MeasurableSpace.generateFrom {t | ∃ j, j ≤ i ∧ s j = t} = MeasurableSpace.generateFrom {s_1 | ∃ n, MeasurableSet s_1}
[PROOFSTEP]
refine' le_antisymm (generateFrom_le _) (generateFrom_le _)
[GOAL]
case h.refine'_1
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
⊢ ∀ (t : Set Ω), t ∈ {t | ∃ j, j ≤ i ∧ s j = t} → MeasurableSet t
[PROOFSTEP]
rintro _ ⟨j, hij, rfl⟩
[GOAL]
case h.refine'_1.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
⊢ MeasurableSet (s j)
[PROOFSTEP]
refine' measurableSet_generateFrom ⟨j, measurableSet_generateFrom ⟨hij, _⟩⟩
[GOAL]
case h.refine'_1.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
⊢ MeasurableSet (s j)
[PROOFSTEP]
rw [comap_eq_generateFrom]
[GOAL]
case h.refine'_1.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
⊢ MeasurableSet (s j)
[PROOFSTEP]
refine' measurableSet_generateFrom ⟨{1}, measurableSet_singleton 1, _⟩
[GOAL]
case h.refine'_1.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
⊢ (Set.indicator (s j) fun x => 1) ⁻¹' {1} = s j
[PROOFSTEP]
ext x
[GOAL]
case h.refine'_1.intro.intro.h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
x : Ω
⊢ x ∈ (Set.indicator (s j) fun x => 1) ⁻¹' {1} ↔ x ∈ s j
[PROOFSTEP]
simp [Set.indicator_const_preimage_eq_union]
[GOAL]
case h.refine'_2
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
⊢ ∀ (t : Set Ω), t ∈ {s_1 | ∃ n, MeasurableSet s_1} → MeasurableSet t
[PROOFSTEP]
rintro t ⟨n, ht⟩
[GOAL]
case h.refine'_2.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
⊢ MeasurableSet t
[PROOFSTEP]
suffices
  MeasurableSpace.generateFrom
      {t | n ≤ i ∧ MeasurableSet[MeasurableSpace.comap ((s n).indicator (fun _ => 1 : Ω → β)) mβ] t} ≤
    MeasurableSpace.generateFrom {t | ∃ (j : ι), j ≤ i ∧ s j = t}
  by exact this _ ht
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
this :
  MeasurableSpace.generateFrom {t | n ≤ i ∧ MeasurableSet t} ≤ MeasurableSpace.generateFrom {t | ∃ j, j ≤ i ∧ s j = t}
⊢ MeasurableSet t
[PROOFSTEP]
exact this _ ht
[GOAL]
case h.refine'_2.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
⊢ MeasurableSpace.generateFrom {t | n ≤ i ∧ MeasurableSet t} ≤ MeasurableSpace.generateFrom {t | ∃ j, j ≤ i ∧ s j = t}
[PROOFSTEP]
refine' generateFrom_le _
[GOAL]
case h.refine'_2.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
⊢ ∀ (t : Set Ω), t ∈ {t | n ≤ i ∧ MeasurableSet t} → MeasurableSet t
[PROOFSTEP]
rintro t ⟨hn, u, _, hu'⟩
[GOAL]
case h.refine'_2.intro.intro.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
⊢ MeasurableSet t
[PROOFSTEP]
obtain heq | heq | heq | heq := Set.indicator_const_preimage (s n) u (1 : β)
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = Set.univ
⊢ MeasurableSet t
case h.refine'_2.intro.intro.intro.intro.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = s n
⊢ MeasurableSet t
case h.refine'_2.intro.intro.intro.intro.inr.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet t
case h.refine'_2.intro.intro.intro.intro.inr.inr.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u ∈ {∅}
⊢ MeasurableSet t
[PROOFSTEP]
pick_goal 4
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inr.inr.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u ∈ {∅}
⊢ MeasurableSet t
case h.refine'_2.intro.intro.intro.intro.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = Set.univ
⊢ MeasurableSet t
case h.refine'_2.intro.intro.intro.intro.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = s n
⊢ MeasurableSet t
case h.refine'_2.intro.intro.intro.intro.inr.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet t
[PROOFSTEP]
rw [Set.mem_singleton_iff] at heq 
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inr.inr.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = ∅
⊢ MeasurableSet t
case h.refine'_2.intro.intro.intro.intro.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = Set.univ
⊢ MeasurableSet t
case h.refine'_2.intro.intro.intro.intro.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = s n
⊢ MeasurableSet t
case h.refine'_2.intro.intro.intro.intro.inr.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet t
[PROOFSTEP]
all_goals rw [heq] at hu' ; rw [← hu']
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inr.inr.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = ∅
⊢ MeasurableSet t
[PROOFSTEP]
rw [heq] at hu' 
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inr.inr.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : ∅ = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = ∅
⊢ MeasurableSet t
[PROOFSTEP]
rw [← hu']
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = Set.univ
⊢ MeasurableSet t
[PROOFSTEP]
rw [heq] at hu' 
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : Set.univ = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = Set.univ
⊢ MeasurableSet t
[PROOFSTEP]
rw [← hu']
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = s n
⊢ MeasurableSet t
[PROOFSTEP]
rw [heq] at hu' 
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : s n = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = s n
⊢ MeasurableSet t
[PROOFSTEP]
rw [← hu']
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inr.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet t
[PROOFSTEP]
rw [heq] at hu' 
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inr.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (s n)ᶜ = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet t
[PROOFSTEP]
rw [← hu']
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inr.inr.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : ∅ = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = ∅
⊢ MeasurableSet ∅
case h.refine'_2.intro.intro.intro.intro.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : Set.univ = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = Set.univ
⊢ MeasurableSet Set.univ
case h.refine'_2.intro.intro.intro.intro.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : s n = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = s n
⊢ MeasurableSet (s n)
case h.refine'_2.intro.intro.intro.intro.inr.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (s n)ᶜ = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet (s n)ᶜ
[PROOFSTEP]
exacts [measurableSet_empty _, MeasurableSet.univ, measurableSet_generateFrom ⟨n, hn, rfl⟩,
  MeasurableSet.compl (measurableSet_generateFrom ⟨n, hn, rfl⟩)]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
⊢ StronglyMeasurable (limitProcess f ℱ μ)
[PROOFSTEP]
rw [limitProcess]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
⊢ StronglyMeasurable
    (if h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) then Classical.choose h
    else 0)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ StronglyMeasurable (Classical.choose h)
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
h : ¬∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ StronglyMeasurable 0
[PROOFSTEP]
exacts [(Classical.choose_spec h).1, stronglyMeasurable_zero]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : Preorder ι
E : Type u_4
inst✝² : Zero E
inst✝¹ : TopologicalSpace E
ℱ✝ : Filtration ι m
f✝ : ι → Ω → E
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
⊢ Memℒp (limitProcess f ℱ μ) p
[PROOFSTEP]
rw [limitProcess]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : Preorder ι
E : Type u_4
inst✝² : Zero E
inst✝¹ : TopologicalSpace E
ℱ✝ : Filtration ι m
f✝ : ι → Ω → E
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
⊢ Memℒp
    (if h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) then Classical.choose h
    else 0)
    p
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : Preorder ι
E : Type u_4
inst✝² : Zero E
inst✝¹ : TopologicalSpace E
ℱ✝ : Filtration ι m
f✝ : ι → Ω → E
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ Memℒp (Classical.choose h) p
[PROOFSTEP]
refine'
  ⟨StronglyMeasurable.aestronglyMeasurable ((Classical.choose_spec h).1.mono (sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _)),
    lt_of_le_of_lt (Lp.snorm_lim_le_liminf_snorm hfm _ (Classical.choose_spec h).2)
      (lt_of_le_of_lt _ (ENNReal.coe_lt_top : ↑R < ∞))⟩
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : Preorder ι
E : Type u_4
inst✝² : Zero E
inst✝¹ : TopologicalSpace E
ℱ✝ : Filtration ι m
f✝ : ι → Ω → E
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ liminf (fun n => snorm (f n) p μ) atTop ≤ ↑R
[PROOFSTEP]
simp_rw [liminf_eq, eventually_atTop]
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : Preorder ι
E : Type u_4
inst✝² : Zero E
inst✝¹ : TopologicalSpace E
ℱ✝ : Filtration ι m
f✝ : ι → Ω → E
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ sSup {a | ∃ a_1, ∀ (b : ℕ), b ≥ a_1 → a ≤ snorm (f b) p μ} ≤ ↑R
[PROOFSTEP]
exact sSup_le fun b ⟨a, ha⟩ => (ha a le_rfl).trans (hbdd _)
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : Preorder ι
E : Type u_4
inst✝² : Zero E
inst✝¹ : TopologicalSpace E
ℱ✝ : Filtration ι m
f✝ : ι → Ω → E
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
h : ¬∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ Memℒp 0 p
[PROOFSTEP]
exact zero_memℒp
