English
If (a^k) ⋅ m = 0 and a is nilpotent, then exp(a) ⋅ m equals the sum over i=0..k-1 of (i!)^{-1} a^i ⋅ m.
Русский
Если (a^k) ⋅ m = 0 и a нильпотентен, то exp(a) ⋅ m равно сумме по i=0..k-1 (i!)^{-1} a^i ⋅ m.
LaTeX
$$exp(a) \cdot m = \sum_{i=0}^{k-1} (i!)^{-1} \cdot a^{i} \cdot m \quad\text{given } (a^{k}) \cdot m = 0 \text{ and } \mathrm{IsNilpotent}(a)$$
Lean4
theorem exp_smul_eq_sum {M : Type*} [AddCommGroup M] [Module A M] [Module ℚ M] {a : A} {m : M} {k : ℕ}
(h : (a ^ k) • m = 0) (hn : IsNilpotent a) : exp a • m = ∑ i ∈ range k, (i.factorial : ℚ)⁻¹ • (a ^ i) • m :=
by
rcases le_or_gt (nilpotencyClass a) k with h₀ | h₀
· simp_rw [exp_eq_sum (pow_eq_zero_of_le h₀ (pow_nilpotencyClass hn)), sum_smul, smul_assoc]
rw [exp, sum_smul, ← sum_range_add_sum_Ico _ (Nat.le_of_succ_le h₀)]
suffices ∑ i ∈ Ico k (nilpotencyClass a), ((i.factorial : ℚ)⁻¹ • (a ^ i)) • m = 0 by
simp_rw [this, add_zero, smul_assoc]
refine sum_eq_zero fun r h₂ ↦ ?_
rw [smul_assoc, ← pow_sub_mul_pow a (mem_Ico.1 h₂).1, mul_smul, h, smul_zero, smul_zero]
