α : Type u_1
β : Type ?u.18790
𝕜 : Type u_3
E : Type u_2
F : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α) (x : E), x ∈ s → HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), x ∈ s → ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : CauchySeq fun s => ∑ b in s, f b x₀
x : E
hx : x ∈ s
⊢ CauchySeq fun s => ∑ b in s, f b x
α : Type u_1
β : Type ?u.18790
𝕜 : Type u_3
E : Type u_2
F : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α) (x : E), x ∈ s → HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), x ∈ s → ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable fun x => f x x₀
x : E
hx : x ∈ s
⊢ Summable fun n => f n x
rw [summable_iff_cauchySeq_finset] at hf0 ⊢
α : Type u_1
β : Type ?u.18790
𝕜 : Type u_3
E : Type u_2
F : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α) (x : E), x ∈ s → HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), x ∈ s → ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : CauchySeq fun s => ∑ b in s, f b x₀
x : E
hx : x ∈ s
A : UniformCauchySeqOn (fun t x => ∑ i in t, f' i x) atTop s
⊢ CauchySeq fun s => ∑ b in s, f b x
α : Type u_1
β : Type ?u.18790
𝕜 : Type u_3
E : Type u_2
F : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α) (x : E), x ∈ s → HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), x ∈ s → ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : CauchySeq fun s => ∑ b in s, f b x₀
x : E
hx : x ∈ s
⊢ CauchySeq fun s => ∑ b in s, f b x
have A : UniformCauchySeqOn (fun t : Finset α => fun x => ∑ i in t, f' i x) atTop s :=
  (tendstoUniformlyOn_tsum hu hf').uniformCauchySeqOn
α : Type u_1
β : Type ?u.18790
𝕜 : Type u_3
E : Type u_2
F : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α) (x : E), x ∈ s → HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), x ∈ s → ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : CauchySeq fun s => ∑ b in s, f b x₀
x : E
hx : x ∈ s
A : UniformCauchySeqOn (fun t x => ∑ i in t, f' i x) atTop s
t : Finset α
y : E
hy : y ∈ s
⊢ HasFDerivAt ((fun t x => ∑ i in t, f i x) t) (∑ i in t, f' i y) y
α : Type u_1
β : Type ?u.18790
𝕜 : Type u_3
E : Type u_2
F : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α) (x : E), x ∈ s → HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), x ∈ s → ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : CauchySeq fun s => ∑ b in s, f b x₀
x : E
hx : x ∈ s
A : UniformCauchySeqOn (fun t x => ∑ i in t, f' i x) atTop s
⊢ CauchySeq fun s => ∑ b in s, f b x
refine cauchy_map_of_uniformCauchySeqOn_fderiv (f := fun t x ↦ ∑ i in t, f i x)
  hs h's A (fun t y hy => ?_) hx₀ hx hf0
no goals
α : Type u_1
β : Type ?u.18790
𝕜 : Type u_3
E : Type u_2
F : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀ x✝ : E
N : ℕ∞
hu : Summable u
hs : IsOpen s
h's : IsPreconnected s
hf : ∀ (n : α) (x : E), x ∈ s → HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), x ∈ s → ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : CauchySeq fun s => ∑ b in s, f b x₀
x : E
hx : x ∈ s
A : UniformCauchySeqOn (fun t x => ∑ i in t, f' i x) atTop s
t : Finset α
y : E
hy : y ∈ s
⊢ HasFDerivAt ((fun t x => ∑ i in t, f i x) t) (∑ i in t, f' i y) y
exact HasFDerivAt.sum fun i _ => hf i y hy