English
A polynomial identity for the even index of Ψ: W.Ψ(2m)·Ψ₂ equals a particular combination of Ψ-values at nearby indices.
Русский
Имеется тождество для чётного индекса Ψ: W.Ψ(2m)·Ψ₂ равняется определённому сочетанию значений Ψ в близких индексах.
LaTeX
$$$W.\\Ψ (2m) \cdot W.\\Ψ_2 = W.\\Ψ (m-1)^2 \cdot W.\\Ψ m \cdot W.\\Ψ (m+2) - W.\\Ψ (m-2) \cdot W.\\Ψ m \cdot W.\\Ψ (m+1)^2$$$
Lean4
theorem Ψ_even (m : ℤ) :
W.Ψ (2 * m) * W.ψ₂ = W.Ψ (m - 1) ^ 2 * W.Ψ m * W.Ψ (m + 2) - W.Ψ (m - 2) * W.Ψ m * W.Ψ (m + 1) ^ 2 :=
by
simp_rw [Ψ, preΨ_even, if_pos <| even_two_mul m, Int.even_add, Int.even_sub, even_two, iff_true, Int.not_even_one,
iff_false]
split_ifs <;> C_simp <;> ring1