English
If a finite family f_i in a Banach algebra commute pairwise, then exp(∑ f_i) equals the product of the exponentials, with the natural ordering given by the commuting relation.
Русский
Если конечное семейство элементов f_i в банаховой алгебре взаимно коммутатирует, то exp(∑ f_i) равняется произведению exp(f_i) (в естественном порядке, учитывая коммютируемость).
LaTeX
$$$\\exp 𝕂\\left(\\sum_{i \\in s} f(i)\\right) = \\prod_{i \\in s} \\exp 𝕂(f(i))$$$
Lean4
/-- In a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`, if a family of elements `f i` mutually
commute then `NormedSpace.exp 𝕂 (∑ i, f i) = ∏ i, NormedSpace.exp 𝕂 (f i)`. -/
theorem exp_sum_of_commute {ι} (s : Finset ι) (f : ι → 𝔸) (h : (s : Set ι).Pairwise (Commute on f)) :
exp 𝕂 (∑ i ∈ s, f i) = s.noncommProd (fun i => exp 𝕂 (f i)) fun _ hi _ hj _ => (h.of_refl hi hj).exp 𝕂 := by
classical
induction s using Finset.induction_on with
| empty => simp
| insert a s ha
ih =>
rw [Finset.noncommProd_insert_of_notMem _ _ _ _ ha, Finset.sum_insert ha, exp_add_of_commute,
ih (h.mono <| Finset.subset_insert _ _)]
refine Commute.sum_right _ _ _ fun i hi => ?_
exact h.of_refl (Finset.mem_insert_self _ _) (Finset.mem_insert_of_mem hi)
