English
The n-th iterate of a LieDerivation applied to the bracket [a,b] satisfies a generalized Leibniz rule, expressed as a sum over all antidiagonal indices with binomial coefficients.
Русский
Кратное применение производной по Lie к скобке [a,b] удовлетворяет обобщенному правилу Лейбница, выражаемому суммой по антидиагоналям с биномиальными коэффициентами.
LaTeX
$$$D^{[n]} [a,b] = \sum_{ij \in \text{antidiagonal } n} {n \choose i} \, [D^{[i]} a, D^{[j]} b]$$$
Lean4
/-- The general Leibniz rule for Lie derivatives. -/
theorem iterate_apply_lie (D : LieDerivation R L L) (n : ℕ) (a b : L) :
D^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, choose n ij.1 • ⁅D^[ij.1] a, D^[ij.2] b⁆ := by
induction n with
| zero => simp
| succ n ih =>
rw [sum_antidiagonal_choose_succ_nsmul (M := L) (fun i j => ⁅D^[i] a, D^[j] b⁆) n]
simp only [Function.iterate_succ_apply', ih, map_sum, map_nsmul, apply_lie_eq_add, smul_add, sum_add_distrib,
add_right_inj]
refine sum_congr rfl fun ⟨i, j⟩ hij ↦ ?_
rw [n.choose_symm_of_eq_add (mem_antidiagonal.1 hij).symm]
