[GOAL]
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ FinStronglyMeasurable f μ
[PROOFSTEP]
borelize G
[GOAL]
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
⊢ FinStronglyMeasurable f μ
[PROOFSTEP]
haveI : SeparableSpace (Set.range f ∪ {0} : Set G) := hf_meas.separableSpace_range_union_singleton
[GOAL]
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
⊢ FinStronglyMeasurable f μ
[PROOFSTEP]
let fs := SimpleFunc.approxOn f hf_meas.measurable (Set.range f ∪ {0}) 0 (by simp)
[GOAL]
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
⊢ 0 ∈ Set.range f ∪ {0}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f (_ : Measurable f) (Set.range f ∪ {0}) 0 (_ : 0 ∈ Set.range f ∪ {0})
⊢ FinStronglyMeasurable f μ
[PROOFSTEP]
refine' ⟨fs, _, _⟩
[GOAL]
case refine'_1
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f (_ : Measurable f) (Set.range f ∪ {0}) 0 (_ : 0 ∈ Set.range f ∪ {0})
⊢ ∀ (n : ℕ), ↑↑μ (support ↑(fs n)) < ⊤
[PROOFSTEP]
have h_fs_Lp : ∀ n, Memℒp (fs n) p μ := SimpleFunc.memℒp_approxOn_range hf_meas.measurable hf
[GOAL]
case refine'_1
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f (_ : Measurable f) (Set.range f ∪ {0}) 0 (_ : 0 ∈ Set.range f ∪ {0})
h_fs_Lp : ∀ (n : ℕ), Memℒp (↑(fs n)) p
⊢ ∀ (n : ℕ), ↑↑μ (support ↑(fs n)) < ⊤
[PROOFSTEP]
exact fun n => (fs n).measure_support_lt_top_of_memℒp (h_fs_Lp n) hp_ne_zero hp_ne_top
[GOAL]
case refine'_2
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f (_ : Measurable f) (Set.range f ∪ {0}) 0 (_ : 0 ∈ Set.range f ∪ {0})
⊢ ∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
[PROOFSTEP]
intro x
[GOAL]
case refine'_2
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f (_ : Measurable f) (Set.range f ∪ {0}) 0 (_ : 0 ∈ Set.range f ∪ {0})
x : α
⊢ Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
[PROOFSTEP]
apply SimpleFunc.tendsto_approxOn
[GOAL]
case refine'_2.hx
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f (_ : Measurable f) (Set.range f ∪ {0}) 0 (_ : 0 ∈ Set.range f ∪ {0})
x : α
⊢ f x ∈ closure (Set.range f ∪ {0})
[PROOFSTEP]
apply subset_closure
[GOAL]
case refine'_2.hx.a
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f (_ : Measurable f) (Set.range f ∪ {0}) 0 (_ : 0 ∈ Set.range f ∪ {0})
x : α
⊢ f x ∈ Set.range f ∪ {0}
[PROOFSTEP]
simp
