Ψ_even — Mathlib

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

Похожие утверждения