xy_succ_succ — Mathlib

English

For a > 1 and n, the pair (x_n, y_n) satisfies both x and y recurrences at n+2 and n alike, i.e.,

Русский

Для a > 1 и n выполняются обе рекуррентности x и y для шагов n+2 и n, т.е.

LaTeX

$$For all a > 1 and n,\n x_n(a, n+2) + x_n(a, n) = 2 a x_n(a, n+1) and\n y_n(a, n+2) + y_n(a, n) = 2 a y_n(a, n+1).$$

Lean4

theorem xy_succ_succ (n) :
    xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1) :=
  by
  have := pellZd_succ_succ a1 n; unfold pellZd at this
  rw [Zsqrtd.nsmul_val (2 * a : ℕ)] at this
  injection this with h₁ h₂
  grind

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