no goals
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.16649
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F
x : E
⊢ ⊤ ≤ FormalMultilinearSeries.radius (fpowerSeries f x)
simp
no goals
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.16649
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F
x y✝ : E
x✝ : y✝ ∈ EMetric.ball 0 ⊤
⊢ HasSum (fun n => ↑(fpowerSeries f x (n + 2)) fun x => y✝)
    (↑f (x + y✝) - ∑ i in Finset.range 2, ↑(fpowerSeries f x i) fun x => y✝)
simp [Finset.sum_range_succ, ← sub_sub, hasSum_zero, fpowerSeries]