no goals
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x : E × F
⊢ ⊤ ≤ FormalMultilinearSeries.radius (fpowerSeriesBilinear f x)
simp
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_3
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✝))
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_3
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✝)
simp only [Finset.sum_range_succ, Finset.sum_range_one, Prod.fst_add, Prod.snd_add,
  f.map_add_add]
no goals
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_3
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✝))
simp [fpowerSeriesBilinear, hasSum_zero]