English
In a commutative Banach algebra, whenever x and y lie in the convergence ball and commute, exp(x+y) = exp(x) exp(y).
Русский
В упорядоченной банаховой алгебре при условии, что x и y лежат в шаре сходления и коммутируют, выполняется exp(x+y) = exp(x) exp(y).
LaTeX
$$$\text{If } x,y \in B(0, \operatorname{radius}(\expSeries 𝕂 𝔸)) \text{ and } Commute x y, \; \exp 𝕂 (x+y) = \exp 𝕂 x \; \exp 𝕂 y$$$
Lean4
/-- In a commutative Banach-algebra `𝔸` over a normed field `𝕂` of characteristic zero,
`NormedSpace.exp 𝕂 (x+y) = (NormedSpace.exp 𝕂 x) * (NormedSpace.exp 𝕂 y)`
for all `x`, `y` in the disk of convergence. -/
theorem exp_add_of_mem_ball [CharZero 𝕂] {x y : 𝔸} (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius)
(hy : y ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : exp 𝕂 (x + y) = exp 𝕂 x * exp 𝕂 y :=
exp_add_of_commute_of_mem_ball (Commute.all x y) hx hy
