English
For any W and integer n, the coefficient of W.preΨ n at the index (n^2 - if Even n then 4 else 1)/2 equals if Even n then n/2 else n.
Русский
Для любого W и целого n коэффициент W.preΨ n при индексе (n^2 - if Even n then 4 else 1)/2 равен (n/2) если n четное, иначе n.
LaTeX
$$ (W.preΨ n).coeff\left(\frac{n^2 - \text{if Even}(n) \text{ then } 4 \text{ else } 1}{2}\right) = \begin{cases} \frac{n}{2}, & \text{Even}(n) \\ n, & \text{not Even}(n) \end{cases} $$
Lean4
@[simp]
theorem coeff_preΨ (n : ℤ) :
(W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) = if Even n then n / 2 else n := by
induction n using Int.negInduction with
| nat n => exact_mod_cast W.preΨ_ofNat n ▸ W.coeff_preΨ' n
| neg ih n =>
simp_rw [preΨ_neg, coeff_neg, Int.natAbs_neg, even_neg]
rcases ih n, n.even_or_odd' with ⟨ih, ⟨n, rfl | rfl⟩⟩ <;>
push_cast [even_two_mul, Int.not_even_two_mul_add_one, Int.neg_ediv_of_dvd ⟨n, rfl⟩] at * <;>
rw [ih]
