no goals
α : Type ?u.941082
β : Type ?u.941085
ι : Type ?u.941088
E : Type ?u.941091
F : Type ?u.941094
𝕜 : Type ?u.941097
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f
n : ℕ
x : β
⊢ 0 ∈ Set.range f ∪ {0}
simp
case hμ
α : Type ?u.941082
β : Type u_2
ι : Type ?u.941088
E : Type u_1
F : Type ?u.941094
𝕜 : Type ?u.941097
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f
⊢ ∀ᵐ (x : β) ∂μ, f x ∈ closure (Set.range f ∪ {0})

case hi
α : Type ?u.941082
β : Type u_2
ι : Type ?u.941088
E : Type u_1
F : Type ?u.941094
𝕜 : Type ?u.941097
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f
⊢ HasFiniteIntegral fun x => f x - 0
α : Type ?u.941082
β : Type u_2
ι : Type ?u.941088
E : Type u_1
F : Type ?u.941094
𝕜 : Type ?u.941097
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f
⊢ Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f fmeas (Set.range f ∪ {0}) 0 (_ : 0 ∈ Set.range f ∪ {0}) n) x - f x‖₊ ∂μ)
    atTop (𝓝 0)
apply tendsto_approxOn_L1_nnnorm fmeas
case hμ.hp
α : Type ?u.941082
β : Type u_2
ι : Type ?u.941088
E : Type u_1
F : Type ?u.941094
𝕜 : Type ?u.941097
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f
⊢ ∀ (x : β), f x ∈ closure (Set.range f ∪ {0})
case hμ
α : Type ?u.941082
β : Type u_2
ι : Type ?u.941088
E : Type u_1
F : Type ?u.941094
𝕜 : Type ?u.941097
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f
⊢ ∀ᵐ (x : β) ∂μ, f x ∈ closure (Set.range f ∪ {0})
apply eventually_of_forall
case hμ.hp
α : Type ?u.941082
β : Type u_2
ι : Type ?u.941088
E : Type u_1
F : Type ?u.941094
𝕜 : Type ?u.941097
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f
x : β
⊢ f x ∈ closure (Set.range f ∪ {0})
case hμ.hp
α : Type ?u.941082
β : Type u_2
ι : Type ?u.941088
E : Type u_1
F : Type ?u.941094
𝕜 : Type ?u.941097
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f
⊢ ∀ (x : β), f x ∈ closure (Set.range f ∪ {0})
intro x
case hμ.hp.a
α : Type ?u.941082
β : Type u_2
ι : Type ?u.941088
E : Type u_1
F : Type ?u.941094
𝕜 : Type ?u.941097
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f
x : β
⊢ f x ∈ Set.range f ∪ {0}
case hμ.hp
α : Type ?u.941082
β : Type u_2
ι : Type ?u.941088
E : Type u_1
F : Type ?u.941094
𝕜 : Type ?u.941097
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f
x : β
⊢ f x ∈ closure (Set.range f ∪ {0})
apply subset_closure
no goals
case hμ.hp.a
α : Type ?u.941082
β : Type u_2
ι : Type ?u.941088
E : Type u_1
F : Type ?u.941094
𝕜 : Type ?u.941097
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f
x : β
⊢ f x ∈ Set.range f ∪ {0}
simp
no goals
case hi
α : Type ?u.941082
β : Type u_2
ι : Type ?u.941088
E : Type u_1
F : Type ?u.941094
𝕜 : Type ?u.941097
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f
⊢ HasFiniteIntegral fun x => f x - 0
simpa using hf.2