English
An alternate formulation of the generalized Leibniz rule expresses D^[n]([a,b]) as a sum over i of binomial coefficients times brackets of iterates on a and b with indices i and n−i.
Русский
Альтернативная формулировка обобщённого правила Лейбница выражает D^[n]([a,b]) как сумму по i биномиальных коэффициентов, взятых от скобок и итератов на a и b с индексами i и n−i.
LaTeX
$$$D^{[n]} [a,b] = \sum_{i=0}^{n} {n \choose i} [D^{[i]} a, D^{[n-i]} b]$$$
Lean4
/-- Alternate version of the general Leibniz rule for Lie derivatives. -/
theorem iterate_apply_lie' (D : LieDerivation R L L) (n : ℕ) (a b : L) :
D^[n] ⁅a, b⁆ = ∑ i ∈ range (n + 1), n.choose i • ⁅D^[i] a, D^[n - i] b⁆ :=
by
rw [iterate_apply_lie D n a b]
exact sum_antidiagonal_eq_sum_range_succ (fun i j ↦ n.choose i • ⁅D^[i] a, D^[j] b⁆) n
