English
The operator (toEnd x)^n on the bracket [y,z] expands as a finite sum over the antidiagonal of indices i,j, involving binomial coefficients and brackets of iterates of ad x and φ x applied to y and z.
Русский
Оператор (toEnd x)^n на скобке [y,z] распадается на конечную сумму по антидиагонали индексов i,j, включая биномиальные коэффициенты и скобки итераций ad x и φ x, применённых к y и z.
LaTeX
$$$((\mathrm{toEnd}_{R,L,M} x)^n)([y,z]) = \sum_{(i,j) \in \mathrm{antidiagonal}(n)} {n \choose i} [ ( (\mathrm{ad}_{R L} x)^i y ), ( (\phi x)^j z ) ]$$$
Lean4
theorem toEnd_pow_lie (x y : L) (z : M) (n : ℕ) :
((φ x) ^ n) ⁅y, z⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅((ad R L x) ^ ij.1) y, ((φ x) ^ ij.2) z⁆ := by
induction n with
| zero => simp
| succ n
ih =>
rw [Finset.sum_antidiagonal_choose_succ_nsmul (fun i j ↦ ⁅((ad R L x) ^ i) y, ((φ x) ^ j) z⁆) n]
simp only [pow_succ', Module.End.mul_apply, ih, map_sum, map_nsmul, toEnd_lie, nsmul_add, sum_add_distrib]
rw [add_comm, add_left_cancel_iff, sum_congr rfl]
rintro ⟨i, j⟩ hij
rw [mem_antidiagonal] at hij
rw [Nat.choose_symm_of_eq_add hij.symm]
