no goals
α : Type ?u.804606
β : Type ?u.804609
ι : Type ?u.804612
E : Type ?u.804615
F : Type ?u.804618
𝕜 : Type ?u.804621
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : Memℒp f p
n : ℕ
⊢ 0 ∈ Set.range f ∪ {0}
simp
no goals
α : Type ?u.804606
β : Type u_2
ι : Type ?u.804612
E : Type u_1
F : Type ?u.804618
𝕜 : Type ?u.804621
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : Memℒp f p
⊢ Tendsto
    (fun n =>
      Memℒp.toLp ↑(approxOn f fmeas (Set.range f ∪ {0}) 0 (_ : 0 ∈ Set.range f ∪ {0}) n)
        (_ : Memℒp (↑(approxOn f fmeas (Set.range f ∪ {0}) 0 (_ : 0 ∈ Set.range f ∪ {0}) n)) p))
    atTop (𝓝 (Memℒp.toLp f hf))
simpa only [Lp.tendsto_Lp_iff_tendsto_ℒp''] using
  tendsto_approxOn_range_Lp_snorm hp_ne_top fmeas hf.2