Pell.yn_add
theorem Pell.yn_add :
∀ {a : ℕ} (a1 : 1 < a) (m n : ℕ), Pell.yn a1 (m + n) = Pell.xn a1 m * Pell.yn a1 n + Pell.yn a1 m * Pell.xn a1 n
The theorem `Pell.yn_add` states that for any natural number `a` greater than 1, and any natural numbers `m` and `n`, the `n`-th element of the Pell `y` sequence with parameter `a`, where `n` is the sum of `m` and `n`, is equal to the product of the `m`-th element of the Pell `x` sequence and the `n`-th element of the Pell `y` sequence, plus the product of the `m`-th element of the Pell `y` sequence and the `n`-th element of the Pell `x` sequence. In mathematical notation, this can be stated as: $y_{m+n} = x_m * y_n + y_m * x_n$ for $a > 1$, where $x_n$ and $y_n$ denote the `n`-th element of the Pell `x` and `y` sequences respectively.
More concisely: For any natural number `a` > 1, the `n`-th element of the Pell `y` sequence with parameter `a` is equal to the sum of the product of the `m`-th element of the Pell `x` sequence and the `n`-th element of the Pell `y` sequence, and the product of the `m`-th element of the Pell `y` sequence and the `n`-th element of the Pell `x` sequence, where `n` is the sum of `m` and `n`. In mathematical notation, $y_{m+n} = x_m * y_n + y_m * x_n$.
|
Pell.yn_succ_succ
theorem Pell.yn_succ_succ :
∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.yn a1 (n + 2) + Pell.yn a1 n = 2 * a * Pell.yn a1 (n + 1)
The theorem `Pell.yn_succ_succ` states that for any natural number `a` greater than 1, and for any natural number `n`, the sum of the `n+2`-th term and the `n`-th term of the Pell `y` sequence for `a` is equal to twice `a` times the `n+1`-th term of the same sequence. This is a recurrence relation for the Pell `y` sequence.
More concisely: For any natural number `a` greater than 1 and natural number `n`, the `(n+2)`-th term of the Pell `y` sequence for `a` equals twice `a` times the `(n+1)`-th term.
|
Pell.isPell_norm
theorem Pell.isPell_norm : ∀ {d : ℤ} {b : ℤ√d}, Pell.IsPell b ↔ b * star b = 1
The theorem `Pell.isPell_norm` states that for any integer `d` and any element `b` of the integer extension of square root of `d` (denoted as `ℤ√d`), `b` satisfies the property of being a solution to the Pell equation if and only if the product of `b` and its conjugate is `1`. The Pell equation is defined as `x^2 - d * y^2 = 1` where `x` and `y` are the real and imaginary parts of the complex number respectively.
More concisely: For an integer `d` and any element `b` in the integer extension of sqrt `d`, `b` is a solution to the Pell equation `x^2 - d * y^2 = 1` if and only if `b` and its conjugate have a product of 1.
|
Pell.pellZd_add
theorem Pell.pellZd_add :
∀ {a : ℕ} (a1 : 1 < a) (m n : ℕ), Pell.pellZd a1 (m + n) = Pell.pellZd a1 m * Pell.pellZd a1 n
The theorem `Pell.pellZd_add` states that for any natural number `a` greater than 1, and for any two natural numbers `m` and `n`, the value of the Pell sequence at the sum of `m` and `n` is equal to the product of the values of the Pell sequence at `m` and `n`. The Pell sequence here is viewed as an element of the integer square root of the Pell number `d`. This is an important property of the Pell sequence in the context of number theory.
More concisely: For any natural number `d` and integers `a > 1`, `m`, `n`, the Pell sequence value at `m + n` is equal to the product of the Pell sequence values at `m` and `n` in the sequence of integer square roots of `d`.
|
Pell.eq_pell
theorem Pell.eq_pell :
∀ {a : ℕ} (a1 : 1 < a) {x y : ℕ}, x * x - Pell.d a1 * y * y = 1 → ∃ n, x = Pell.xn a1 n ∧ y = Pell.yn a1 n := by
sorry
The theorem `Pell.eq_pell` states that for any natural number `a` greater than 1, and for any natural numbers `x` and `y` that satisfy the Pell's equation (i.e., `x * x - Pell.d a1 * y * y = 1`), there exists a natural number `n` such that `x` and `y` are the `n`th numbers in the Pell `x` and `y` sequences respectively. These sequences are defined in terms of `a` and the recursive function `Pell.pell`. Essentially, it says that every solution to the Pell's equation can be generated from the initial solution `(1,0)` using the recursion `Pell.pell`.
More concisely: For any natural number `a` greater than 1 and any solutions `x, y` to the Pell equation `x^2 - a*y^2 = 1`, there exists a natural number `n` such that `(x, y)` is the `n`th term in the Pell sequence `(x, y) = Pell.pell (1, 0) (a)`.
|
Pell.strictMono_y
theorem Pell.strictMono_y : ∀ {a : ℕ} (a1 : 1 < a), StrictMono (Pell.yn a1)
The theorem `Pell.strictMono_y` states that for all natural numbers `a` such that `a > 1`, the function `Pell.yn` is strictly monotone. In other words, for any two natural numbers `m` and `n` where `m < n`, the value of `Pell.yn` at `m` is strictly less than the value of `Pell.yn` at `n`. Here, `Pell.yn` is the Pell `y` sequence defined for natural numbers `a` greater than 1.
More concisely: For all natural numbers `a > 1` and any `m, n` with `m < n`, `Pell.yn` (a, m) < `Pell.yn` (a, n).
|