α : Type u_1
β : Type u_2
𝕜 : Type ?u.260
E : Type ?u.263
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (n : Finset α) in atTop, ∀ (x : β), x ∈ s → dist (∑' (n : α), f n x) (∑ n in n, f n x) < ε
α : Type u_1
β : Type u_2
𝕜 : Type ?u.260
E : Type ?u.263
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn (fun t x => ∑ n in t, f n x) (fun x => ∑' (n : α), f n x) atTop s
refine' tendstoUniformlyOn_iff.2 fun ε εpos => _
case h
α : Type u_1
β : Type u_2
𝕜 : Type ?u.260
E : Type ?u.263
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : (∑' (b : { x // ¬x ∈ t }), u ↑b) < ε
x : β
hx : x ∈ s
⊢ dist (∑' (n : α), f n x) (∑ n in t, f n x) < ε
α : Type u_1
β : Type u_2
𝕜 : Type ?u.260
E : Type ?u.263
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (n : Finset α) in atTop, ∀ (x : β), x ∈ s → dist (∑' (n : α), f n x) (∑ n in n, f n x) < ε
filter_upwards [(tendsto_order.1 (tendsto_tsum_compl_atTop_zero u)).2 _ εpos]with t ht x hx
case h
α : Type u_1
β : Type u_2
𝕜 : Type ?u.260
E : Type ?u.263
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : (∑' (b : { x // ¬x ∈ t }), u ↑b) < ε
x : β
hx : x ∈ s
A : Summable fun n => ‖f n x‖
⊢ dist (∑' (n : α), f n x) (∑ n in t, f n x) < ε
case h
α : Type u_1
β : Type u_2
𝕜 : Type ?u.260
E : Type ?u.263
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : (∑' (b : { x // ¬x ∈ t }), u ↑b) < ε
x : β
hx : x ∈ s
⊢ dist (∑' (n : α), f n x) (∑ n in t, f n x) < ε
have A : Summable fun n => ‖f n x‖ :=
  summable_of_nonneg_of_le (fun n => norm_nonneg _) (fun n => hfu n x hx) hu
case h
α : Type u_1
β : Type u_2
𝕜 : Type ?u.260
E : Type ?u.263
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : (∑' (b : { x // ¬x ∈ t }), u ↑b) < ε
x : β
hx : x ∈ s
A : Summable fun n => ‖f n x‖
⊢ ‖∑' (x_1 : { x // ¬x ∈ t }), f (↑x_1) x‖ < ε
case h
α : Type u_1
β : Type u_2
𝕜 : Type ?u.260
E : Type ?u.263
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : (∑' (b : { x // ¬x ∈ t }), u ↑b) < ε
x : β
hx : x ∈ s
A : Summable fun n => ‖f n x‖
⊢ dist (∑' (n : α), f n x) (∑ n in t, f n x) < ε
rw [dist_eq_norm, ← sum_add_tsum_subtype_compl (summable_of_summable_norm A) t, add_sub_cancel']
α : Type u_1
β : Type u_2
𝕜 : Type ?u.260
E : Type ?u.263
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : (∑' (b : { x // ¬x ∈ t }), u ↑b) < ε
x : β
hx : x ∈ s
A : Summable fun n => ‖f n x‖
⊢ ‖∑' (x_1 : { x // ¬x ∈ t }), f (↑x_1) x‖ ≤ ∑' (b : { x // ¬x ∈ t }), u ↑b
case h
α : Type u_1
β : Type u_2
𝕜 : Type ?u.260
E : Type ?u.263
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : (∑' (b : { x // ¬x ∈ t }), u ↑b) < ε
x : β
hx : x ∈ s
A : Summable fun n => ‖f n x‖
⊢ ‖∑' (x_1 : { x // ¬x ∈ t }), f (↑x_1) x‖ < ε
apply lt_of_le_of_lt _ ht
α : Type u_1
β : Type u_2
𝕜 : Type ?u.260
E : Type ?u.263
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : (∑' (b : { x // ¬x ∈ t }), u ↑b) < ε
x : β
hx : x ∈ s
A : Summable fun n => ‖f n x‖
⊢ (∑' (i : ↑fun x => x ∈ t → False), ‖f (↑i) x‖) ≤ ∑' (b : { x // ¬x ∈ t }), u ↑b
α : Type u_1
β : Type u_2
𝕜 : Type ?u.260
E : Type ?u.263
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : (∑' (b : { x // ¬x ∈ t }), u ↑b) < ε
x : β
hx : x ∈ s
A : Summable fun n => ‖f n x‖
⊢ ‖∑' (x_1 : { x // ¬x ∈ t }), f (↑x_1) x‖ ≤ ∑' (b : { x // ¬x ∈ t }), u ↑b
apply (norm_tsum_le_tsum_norm (A.subtype _)).trans
no goals
α : Type u_1
β : Type u_2
𝕜 : Type ?u.260
E : Type ?u.263
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α) (x : β), x ∈ s → ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : (∑' (b : { x // ¬x ∈ t }), u ↑b) < ε
x : β
hx : x ∈ s
A : Summable fun n => ‖f n x‖
⊢ (∑' (i : ↑fun x => x ∈ t → False), ‖f (↑i) x‖) ≤ ∑' (b : { x // ¬x ∈ t }), u ↑b
exact tsum_le_tsum (fun n => hfu _ _ hx) (A.subtype _) (hu.subtype _)