Φ_ofNat — Mathlib

English

Similar parity-based formula for Φ with natural indices, illustrating the pattern of Φ at n+1.

Русский

Аналогичная формула для Φ с натуральными индексами, иллюстрирующая образец Φ при n+1.

LaTeX

$$$W.\\Φ(n cast + 1) = X \\cdot W.preΨ'(n cast + 1)^2 \\cdot (\\text{Even } n \text{ ? } 1 : W.\\Ψ_2^2) - W.preΨ'(n cast + 2) \\cdot W.preΨ'(n cast) \\cdot (\\text{Even } n \text{ ? } W.\\Ψ_2^2 : 1)$$$

Lean4

@[simp]
theorem Φ_ofNat (n : ℕ) :
    W.Φ (n + 1) =
      X * W.preΨ' (n + 1) ^ 2 * (if Even n then 1 else W.Ψ₂Sq) -
        W.preΨ' (n + 2) * W.preΨ' n * (if Even n then W.Ψ₂Sq else 1) :=
  by
  rw [Φ, add_sub_cancel_right]
  norm_cast
  simp_rw [ΨSq_ofNat, Nat.even_add_one, ite_not, ← mul_assoc, preΨ_ofNat]

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