𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
⊢ r - ↑‖y‖₊ ≤ FormalMultilinearSeries.radius p - ↑‖y‖₊
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
⊢ r - ↑‖y‖₊ ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.changeOrigin p y)
apply le_trans _ p.changeOrigin_radius
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
⊢ r - ↑‖y‖₊ ≤ FormalMultilinearSeries.radius p - ↑‖y‖₊
exact tsub_le_tsub hf.r_le le_rfl
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
⊢ 0 < r - ↑‖y‖₊
simp [h]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
z : E
hz : z ∈ EMetric.ball 0 (r - ↑‖y‖₊)
this : f (x + y + z) = FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z
⊢ HasSum (fun n => ↑(FormalMultilinearSeries.changeOrigin p y n) fun x => z) (f (x + y + z))
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
z : E
hz : z ∈ EMetric.ball 0 (r - ↑‖y‖₊)
⊢ HasSum (fun n => ↑(FormalMultilinearSeries.changeOrigin p y n) fun x => z) (f (x + y + z))
have : f (x + y + z) =
    FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z := by
  rw [mem_emetric_ball_zero_iff, lt_tsub_iff_right, add_comm] at hz
  rw [p.changeOrigin_eval (hz.trans_le hf.r_le), add_assoc, hf.sum]
  refine' mem_emetric_ball_zero_iff.2 (lt_of_le_of_lt _ hz)
  exact_mod_cast nnnorm_add_le y z
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
z : E
hz : z ∈ EMetric.ball 0 (r - ↑‖y‖₊)
this : f (x + y + z) = FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z
⊢ HasSum (fun n => ↑(FormalMultilinearSeries.changeOrigin p y n) fun x => z)
    (FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z)
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
z : E
hz : z ∈ EMetric.ball 0 (r - ↑‖y‖₊)
this : f (x + y + z) = FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z
⊢ HasSum (fun n => ↑(FormalMultilinearSeries.changeOrigin p y n) fun x => z) (f (x + y + z))
rw [this]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
z : E
hz : z ∈ EMetric.ball 0 (r - ↑‖y‖₊)
this : f (x + y + z) = FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z
⊢ z ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (FormalMultilinearSeries.changeOrigin p y))
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
z : E
hz : z ∈ EMetric.ball 0 (r - ↑‖y‖₊)
this : f (x + y + z) = FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z
⊢ HasSum (fun n => ↑(FormalMultilinearSeries.changeOrigin p y n) fun x => z)
    (FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z)
apply (p.changeOrigin y).hasSum
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
z : E
hz : z ∈ EMetric.ball 0 (r - ↑‖y‖₊)
this : f (x + y + z) = FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z
⊢ r - ↑‖y‖₊ ≤ FormalMultilinearSeries.radius p - ↑‖y‖₊
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
z : E
hz : z ∈ EMetric.ball 0 (r - ↑‖y‖₊)
this : f (x + y + z) = FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z
⊢ z ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (FormalMultilinearSeries.changeOrigin p y))
refine' EMetric.ball_subset_ball (le_trans _ p.changeOrigin_radius) hz
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
z : E
hz : z ∈ EMetric.ball 0 (r - ↑‖y‖₊)
this : f (x + y + z) = FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z
⊢ r - ↑‖y‖₊ ≤ FormalMultilinearSeries.radius p - ↑‖y‖₊
exact tsub_le_tsub hf.r_le le_rfl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
z : E
hz✝ : ↑‖z‖₊ < r - ↑‖y‖₊
hz : ↑‖y‖₊ + ↑‖z‖₊ < r
⊢ f (x + y + z) = FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
z : E
hz : z ∈ EMetric.ball 0 (r - ↑‖y‖₊)
⊢ f (x + y + z) = FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z
rw [mem_emetric_ball_zero_iff, lt_tsub_iff_right, add_comm] at hz
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
z : E
hz✝ : ↑‖z‖₊ < r - ↑‖y‖₊
hz : ↑‖y‖₊ + ↑‖z‖₊ < r
⊢ y + z ∈ EMetric.ball 0 r
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
z : E
hz✝ : ↑‖z‖₊ < r - ↑‖y‖₊
hz : ↑‖y‖₊ + ↑‖z‖₊ < r
⊢ f (x + y + z) = FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z
rw [p.changeOrigin_eval (hz.trans_le hf.r_le), add_assoc, hf.sum]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
z : E
hz✝ : ↑‖z‖₊ < r - ↑‖y‖₊
hz : ↑‖y‖₊ + ↑‖z‖₊ < r
⊢ ↑‖y + z‖₊ ≤ ↑‖y‖₊ + ↑‖z‖₊
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
z : E
hz✝ : ↑‖z‖₊ < r - ↑‖y‖₊
hz : ↑‖y‖₊ + ↑‖z‖₊ < r
⊢ y + z ∈ EMetric.ball 0 r
refine' mem_emetric_ball_zero_iff.2 (lt_of_le_of_lt _ hz)
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2340152
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
z : E
hz✝ : ↑‖z‖₊ < r - ↑‖y‖₊
hz : ↑‖y‖₊ + ↑‖z‖₊ < r
⊢ ↑‖y + z‖₊ ≤ ↑‖y‖₊ + ↑‖z‖₊
exact_mod_cast nnnorm_add_le y z