case pos
𝕂 : Type u_2
𝔸 : Type u_1
𝔹 : Type ?u.98423
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
h : FormalMultilinearSeries.radius (expSeries 𝕂 𝔸) = 0
⊢ AnalyticAt 𝕂 (exp 𝕂) x

case neg
𝕂 : Type u_2
𝔸 : Type u_1
𝔹 : Type ?u.98423
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
h : ¬FormalMultilinearSeries.radius (expSeries 𝕂 𝔸) = 0
⊢ AnalyticAt 𝕂 (exp 𝕂) x
𝕂 : Type u_2
𝔸 : Type u_1
𝔹 : Type ?u.98423
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ AnalyticAt 𝕂 (exp 𝕂) x
by_cases h : (expSeries 𝕂 𝔸).radius = 0
case pos
𝕂 : Type u_2
𝔸 : Type u_1
𝔹 : Type ?u.98423
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 0
h : FormalMultilinearSeries.radius (expSeries 𝕂 𝔸) = 0
⊢ AnalyticAt 𝕂 (exp 𝕂) x
case pos
𝕂 : Type u_2
𝔸 : Type u_1
𝔹 : Type ?u.98423
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
h : FormalMultilinearSeries.radius (expSeries 𝕂 𝔸) = 0
⊢ AnalyticAt 𝕂 (exp 𝕂) x
rw [h] at hx
no goals
case pos
𝕂 : Type u_2
𝔸 : Type u_1
𝔹 : Type ?u.98423
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 0
h : FormalMultilinearSeries.radius (expSeries 𝕂 𝔸) = 0
⊢ AnalyticAt 𝕂 (exp 𝕂) x
exact (ENNReal.not_lt_zero hx).elim
case neg
𝕂 : Type u_2
𝔸 : Type u_1
𝔹 : Type ?u.98423
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
h✝ : ¬FormalMultilinearSeries.radius (expSeries 𝕂 𝔸) = 0
h : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ AnalyticAt 𝕂 (exp 𝕂) x
case neg
𝕂 : Type u_2
𝔸 : Type u_1
𝔹 : Type ?u.98423
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
h : ¬FormalMultilinearSeries.radius (expSeries 𝕂 𝔸) = 0
⊢ AnalyticAt 𝕂 (exp 𝕂) x
have h := pos_iff_ne_zero.mpr h
no goals
case neg
𝕂 : Type u_2
𝔸 : Type u_1
𝔹 : Type ?u.98423
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
h✝ : ¬FormalMultilinearSeries.radius (expSeries 𝕂 𝔸) = 0
h : 0 < FormalMultilinearSeries.radius (expSeries 𝕂 𝔸)
⊢ AnalyticAt 𝕂 (exp 𝕂) x
exact (hasFPowerSeriesOnBall_exp_of_radius_pos h).analyticAt_of_mem hx