[GOAL]
𝕜 : 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_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F
x : E
⊢ ⊤ ≤ FormalMultilinearSeries.radius (fpowerSeries f x)
[PROOFSTEP]
simp
[GOAL]
𝕜 : 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_4
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✝)
[PROOFSTEP]
simp [Finset.sum_range_succ, ← sub_sub, hasSum_zero, fpowerSeries]
[GOAL]
𝕜 : 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_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x : E × F
⊢ ⊤ ≤ FormalMultilinearSeries.radius (fpowerSeriesBilinear f x)
[PROOFSTEP]
simp
[GOAL]
𝕜 : 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_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x y✝ : E × F
x✝ : y✝ ∈ EMetric.ball 0 ⊤
⊢ HasSum (fun n => ↑(fpowerSeriesBilinear f x (n + 3)) fun x => y✝)
    (↑(↑f (x + y✝).fst) (x + y✝).snd - ∑ i in Finset.range 3, ↑(fpowerSeriesBilinear f x i) fun x => y✝)
[PROOFSTEP]
simp only [Finset.sum_range_succ, Finset.sum_range_one, Prod.fst_add, Prod.snd_add, f.map_add_add]
[GOAL]
𝕜 : 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_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x y✝ : E × F
x✝ : y✝ ∈ EMetric.ball 0 ⊤
⊢ HasSum (fun n => ↑(fpowerSeriesBilinear f x (n + 3)) fun x => y✝)
    (↑(↑f x.fst) x.snd + ↑(↑(deriv₂ f) (x.fst, x.snd)) (y✝.fst, y✝.snd) + ↑(↑f y✝.fst) y✝.snd -
      ((((∑ x_1 in Finset.range 0, ↑(fpowerSeriesBilinear f x x_1) fun x => y✝) +
            ↑(fpowerSeriesBilinear f x 0) fun x => y✝) +
          ↑(fpowerSeriesBilinear f x 1) fun x => y✝) +
        ↑(fpowerSeriesBilinear f x 2) fun x => y✝))
[PROOFSTEP]
simp [fpowerSeriesBilinear, hasSum_zero]
