case pos
ι : Type u_1
α : Type ?u.16948
E : Type u_2
F : Type ?u.16954
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : Summable f
⊢ ‖∑' (i : ι), f i‖ ≤ a

case neg
ι : Type u_1
α : Type ?u.16948
E : Type u_2
F : Type ?u.16954
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : ¬Summable f
⊢ ‖∑' (i : ι), f i‖ ≤ a
ι : Type u_1
α : Type ?u.16948
E : Type u_2
F : Type ?u.16954
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ ‖∑' (i : ι), f i‖ ≤ a
by_cases hf : Summable f
no goals
case pos
ι : Type u_1
α : Type ?u.16948
E : Type u_2
F : Type ?u.16954
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : Summable f
⊢ ‖∑' (i : ι), f i‖ ≤ a
exact hf.hasSum.norm_le_of_bounded hg h
case neg
ι : Type u_1
α : Type ?u.16948
E : Type u_2
F : Type ?u.16954
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : ¬Summable f
⊢ 0 ≤ a
case neg
ι : Type u_1
α : Type ?u.16948
E : Type u_2
F : Type ?u.16954
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : ¬Summable f
⊢ ‖∑' (i : ι), f i‖ ≤ a
rw [tsum_eq_zero_of_not_summable hf, norm_zero]
no goals
case neg
ι : Type u_1
α : Type ?u.16948
E : Type u_2
F : Type ?u.16954
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : ¬Summable f
⊢ 0 ≤ a
exact ge_of_tendsto' hg fun s => sum_nonneg fun i _hi => (norm_nonneg _).trans (h i)