α : Type u_1
β : Type ?u.340703
γ : Type ?u.340706
f : α → ℝ
hf : Summable f
⊢ Summable fun a => ↑(Real.toNNReal (f a))
α : Type u_1
β : Type ?u.340703
γ : Type ?u.340706
f : α → ℝ
hf : Summable f
⊢ Summable fun n => Real.toNNReal (f n)
apply NNReal.summable_coe.1
α : Type u_1
β : Type ?u.340703
γ : Type ?u.340706
f : α → ℝ
hf : Summable f
n : α
⊢ ↑(Real.toNNReal (f n)) ≤ Abs.abs (f n)
α : Type u_1
β : Type ?u.340703
γ : Type ?u.340706
f : α → ℝ
hf : Summable f
⊢ Summable fun a => ↑(Real.toNNReal (f a))
refine' summable_of_nonneg_of_le (fun n => NNReal.coe_nonneg _) (fun n => _) hf.abs
no goals
α : Type u_1
β : Type ?u.340703
γ : Type ?u.340706
f : α → ℝ
hf : Summable f
n : α
⊢ ↑(Real.toNNReal (f n)) ≤ Abs.abs (f n)
simp only [le_abs_self, Real.coe_toNNReal', max_le_iff, abs_nonneg, and_self_iff]