English
For any integer m, the odd index Ψ(2m+1) satisfies a decomposition into Ψ-values at m±2 and m with a correction term involving preΨ and Ψ₂Sq.
Русский
Для целого m нечётный Ψ(2m+1) распадается на сумму Ψ–значений с аргументами m±2 и m и с поправочным членом, включающим preΨ и Ψ₂Sq.
LaTeX
$$$W.\\Ψ(2m+1) = W.\\Ψ(m+2)\cdot W.\\Ψ(m)^3 - W.\\Ψ(m-1)\cdot W.\\Ψ(m+1)^3 + W.toAffine.polynomial \cdot (16 \cdot W.toAffine.polynomial - 8 \cdot W.\\ψ_2^2) \cdot C(\text{if Even } m \text{ then } W.preΨ(m+2)\cdot W.preΨ m^3 \text{ else } -W.preΨ(m-1)\cdot W.preΨ(m+1)^3) $$$
Lean4
theorem Ψ_odd (m : ℤ) :
W.Ψ (2 * m + 1) =
W.Ψ (m + 2) * W.Ψ m ^ 3 - W.Ψ (m - 1) * W.Ψ (m + 1) ^ 3 +
W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) *
C (if Even m then W.preΨ (m + 2) * W.preΨ m ^ 3 else -W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3) :=
by
simp_rw [Ψ, preΨ_odd, if_neg m.not_even_two_mul_add_one, Int.even_add, Int.even_sub, even_two, iff_true,
Int.not_even_one, iff_false]
split_ifs <;> C_simp <;> rw [C_Ψ₂Sq] <;> ring1
