no goals
E : Type u_2
ι : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
⊢ DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) U
classical
have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn
refine' hc.differentiableOn (eventually_of_forall fun s => _) hU
exact DifferentiableOn.sum fun i _ => hf i
E : Type u_2
ι : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
hc : TendstoLocallyUniformlyOn (fun t x => Finset.sum t fun n => F n x) (fun x => ∑' (n : ι), F n x) atTop U
⊢ DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) U
E : Type u_2
ι : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
⊢ DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) U
have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn
E : Type u_2
ι : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
hc : TendstoLocallyUniformlyOn (fun t x => Finset.sum t fun n => F n x) (fun x => ∑' (n : ι), F n x) atTop U
s : Finset ι
⊢ DifferentiableOn ℂ (fun x => Finset.sum s fun n => F n x) U
E : Type u_2
ι : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
hc : TendstoLocallyUniformlyOn (fun t x => Finset.sum t fun n => F n x) (fun x => ∑' (n : ι), F n x) atTop U
⊢ DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) U
refine' hc.differentiableOn (eventually_of_forall fun s => _) hU
no goals
E : Type u_2
ι : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
hc : TendstoLocallyUniformlyOn (fun t x => Finset.sum t fun n => F n x) (fun x => ∑' (n : ι), F n x) atTop U
s : Finset ι
⊢ DifferentiableOn ℂ (fun x => Finset.sum s fun n => F n x) U
exact DifferentiableOn.sum fun i _ => hf i