𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2353891
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 ∈ EMetric.ball x r
this : ↑‖y - x‖₊ < r
⊢ AnalyticAt 𝕜 f y
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2353891
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 ∈ EMetric.ball x r
⊢ AnalyticAt 𝕜 f y
have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_coe_nnnorm_sub] using h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2353891
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 ∈ EMetric.ball x r
this✝ : ↑‖y - x‖₊ < r
this : HasFPowerSeriesOnBall f (FormalMultilinearSeries.changeOrigin p (y - x)) (x + (y - x)) (r - ↑‖y - x‖₊)
⊢ AnalyticAt 𝕜 f y
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2353891
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 ∈ EMetric.ball x r
this : ↑‖y - x‖₊ < r
⊢ AnalyticAt 𝕜 f y
have := hf.changeOrigin this
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2353891
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 ∈ EMetric.ball x r
this✝ : ↑‖y - x‖₊ < r
this : HasFPowerSeriesOnBall f (FormalMultilinearSeries.changeOrigin p (y - x)) y (r - ↑‖y - x‖₊)
⊢ AnalyticAt 𝕜 f y
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2353891
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 ∈ EMetric.ball x r
this✝ : ↑‖y - x‖₊ < r
this : HasFPowerSeriesOnBall f (FormalMultilinearSeries.changeOrigin p (y - x)) (x + (y - x)) (r - ↑‖y - x‖₊)
⊢ AnalyticAt 𝕜 f y
rw [add_sub_cancel'_right] at this
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2353891
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 ∈ EMetric.ball x r
this✝ : ↑‖y - x‖₊ < r
this : HasFPowerSeriesOnBall f (FormalMultilinearSeries.changeOrigin p (y - x)) y (r - ↑‖y - x‖₊)
⊢ AnalyticAt 𝕜 f y
exact this.analyticAt
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.2353891
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 ∈ EMetric.ball x r
⊢ ↑‖y - x‖₊ < r
simpa [edist_eq_coe_nnnorm_sub] using h