English
The exponential map is analytic at every point in the ball of convergence.
Русский
Экспонента analytic в каждой точке шара сходимости.
LaTeX
$$AnalyticAt 𝕂 (\\exp 𝕂) x$$
Lean4
/-- In a Banach-algebra `𝔸` over a normed field `𝕂` of characteristic zero, if `x` and `y` are
in the disk of convergence and commute, then
`NormedSpace.exp 𝕂 (x + y) = (NormedSpace.exp 𝕂 x) * (NormedSpace.exp 𝕂 y)`. -/
theorem exp_add_of_commute_of_mem_ball [CharZero 𝕂] {x y : 𝔸} (hxy : Commute x y)
(hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) (hy : y ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
exp 𝕂 (x + y) = exp 𝕂 x * exp 𝕂 y :=
by
rw [exp_eq_tsum,
tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm (norm_expSeries_summable_of_mem_ball' x hx)
(norm_expSeries_summable_of_mem_ball' y hy)]
dsimp only
conv_lhs =>
congr
ext
rw [hxy.add_pow' _, Finset.smul_sum]
refine tsum_congr fun n => Finset.sum_congr rfl fun kl hkl => ?_
rw [← Nat.cast_smul_eq_nsmul 𝕂, smul_smul, smul_mul_smul_comm, ← Finset.mem_antidiagonal.mp hkl, Nat.cast_add_choose,
Finset.mem_antidiagonal.mp hkl]
congr 1
field_simp [n.factorial_ne_zero]
