mathlib documentation

number_theory.pell

@[simp]
theorem pell.d_pos {a : } (a1 : 1 < a) :
0 < d a1

@[nolint]
def pell.pell {a : } :
1 < a ×

The Pell sequences, defined together in mutual recursion.

Equations
def pell.xn {a : } :
1 < a

The Pell x sequence.

Equations
def pell.yn {a : } :
1 < a

The Pell y sequence.

Equations
@[simp]
theorem pell.pell_val {a : } (a1 : 1 < a) (n : ) :
pell.pell a1 n = (pell.xn a1 n, pell.yn a1 n)

@[simp]
theorem pell.xn_zero {a : } (a1 : 1 < a) :
pell.xn a1 0 = 1

@[simp]
theorem pell.yn_zero {a : } (a1 : 1 < a) :
pell.yn a1 0 = 0

@[simp]
theorem pell.xn_succ {a : } (a1 : 1 < a) (n : ) :
pell.xn a1 (n + 1) = (pell.xn a1 n) * a + (d a1) * pell.yn a1 n

@[simp]
theorem pell.yn_succ {a : } (a1 : 1 < a) (n : ) :
pell.yn a1 (n + 1) = pell.xn a1 n + (pell.yn a1 n) * a

@[simp]
theorem pell.xn_one {a : } (a1 : 1 < a) :
pell.xn a1 1 = a

@[simp]
theorem pell.yn_one {a : } (a1 : 1 < a) :
pell.yn a1 1 = 1

def pell.xz {a : } :
1 < a

Equations
def pell.yz {a : } :
1 < a

Equations
def pell.az {a : } :
1 < a

Equations
theorem pell.asq_pos {a : } :
1 < a0 < a * a

theorem pell.dz_val {a : } (a1 : 1 < a) :
(d a1) = (pell.az a1) * pell.az a1 - 1

@[simp]
theorem pell.xz_succ {a : } (a1 : 1 < a) (n : ) :
pell.xz a1 (n + 1) = (pell.xz a1 n) * pell.az a1 + ((d a1)) * pell.yz a1 n

@[simp]
theorem pell.yz_succ {a : } (a1 : 1 < a) (n : ) :
pell.yz a1 (n + 1) = pell.xz a1 n + (pell.yz a1 n) * pell.az a1

def pell.pell_zd {a : } (a1 : 1 < a) :
ℤ√(d a1)

The Pell sequence can also be viewed as an element of ℤ√d

Equations
@[simp]
theorem pell.pell_zd_re {a : } (a1 : 1 < a) (n : ) :
(pell.pell_zd a1 n).re = (pell.xn a1 n)

@[simp]
theorem pell.pell_zd_im {a : } (a1 : 1 < a) (n : ) :
(pell.pell_zd a1 n).im = (pell.yn a1 n)

def pell.is_pell {a : } (a1 : 1 < a) :
ℤ√(d a1) → Prop

The property of being a solution to the Pell equation, expressed as a property of elements of ℤ√d.

Equations
theorem pell.is_pell_nat {a : } (a1 : 1 < a) {x y : } :
pell.is_pell a1 {re := x, im := y} x * x - ((d a1) * y) * y = 1

theorem pell.is_pell_norm {a : } (a1 : 1 < a) {b : ℤ√(d a1)} :
pell.is_pell a1 b b * b.conj = 1

theorem pell.is_pell_mul {a : } (a1 : 1 < a) {b c : ℤ√(d a1)} :
pell.is_pell a1 bpell.is_pell a1 cpell.is_pell a1 (b * c)

theorem pell.is_pell_conj {a : } (a1 : 1 < a) {b : ℤ√(d a1)} :

@[simp]
theorem pell.pell_zd_succ {a : } (a1 : 1 < a) (n : ) :
pell.pell_zd a1 (n + 1) = (pell.pell_zd a1 n) * {re := a, im := 1}

theorem pell.is_pell_one {a : } (a1 : 1 < a) :
pell.is_pell a1 {re := a, im := 1}

theorem pell.is_pell_pell_zd {a : } (a1 : 1 < a) (n : ) :

@[simp]
theorem pell.pell_eqz {a : } (a1 : 1 < a) (n : ) :
(pell.xz a1 n) * pell.xz a1 n - (((d a1)) * pell.yz a1 n) * pell.yz a1 n = 1

@[simp]
theorem pell.pell_eq {a : } (a1 : 1 < a) (n : ) :
(pell.xn a1 n) * pell.xn a1 n - ((d a1) * pell.yn a1 n) * pell.yn a1 n = 1

@[instance]
def pell.dnsq {a : } (a1 : 1 < a) :

theorem pell.xn_ge_a_pow {a : } (a1 : 1 < a) (n : ) :
a ^ n pell.xn a1 n

theorem pell.n_lt_a_pow {a : } (a1 : 1 < a) (n : ) :
n < a ^ n

theorem pell.n_lt_xn {a : } (a1 : 1 < a) (n : ) :
n < pell.xn a1 n

theorem pell.x_pos {a : } (a1 : 1 < a) (n : ) :
0 < pell.xn a1 n

theorem pell.eq_pell_lem {a : } (a1 : 1 < a) (n : ) (b : ℤ√(d a1)) :
1 bpell.is_pell a1 bb pell.pell_zd a1 n(∃ (n : ), b = pell.pell_zd a1 n)

theorem pell.eq_pell_zd {a : } (a1 : 1 < a) (b : ℤ√(d a1)) :
1 bpell.is_pell a1 b(∃ (n : ), b = pell.pell_zd a1 n)

theorem pell.eq_pell {a : } (a1 : 1 < a) {x y : } :
x * x - ((d a1) * y) * y = 1(∃ (n : ), x = pell.xn a1 n y = pell.yn a1 n)

theorem pell.pell_zd_add {a : } (a1 : 1 < a) (m n : ) :
pell.pell_zd a1 (m + n) = (pell.pell_zd a1 m) * pell.pell_zd a1 n

theorem pell.xn_add {a : } (a1 : 1 < a) (m n : ) :
pell.xn a1 (m + n) = (pell.xn a1 m) * pell.xn a1 n + ((d a1) * pell.yn a1 m) * pell.yn a1 n

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

theorem pell.pell_zd_sub {a : } (a1 : 1 < a) {m n : } :
n mpell.pell_zd a1 (m - n) = (pell.pell_zd a1 m) * (pell.pell_zd a1 n).conj

theorem pell.xz_sub {a : } (a1 : 1 < a) {m n : } :
n mpell.xz a1 (m - n) = (pell.xz a1 m) * pell.xz a1 n - (((d a1)) * pell.yz a1 m) * pell.yz a1 n

theorem pell.yz_sub {a : } (a1 : 1 < a) {m n : } :
n mpell.yz a1 (m - n) = (pell.xz a1 n) * pell.yz a1 m - (pell.xz a1 m) * pell.yz a1 n

theorem pell.xy_coprime {a : } (a1 : 1 < a) (n : ) :
(pell.xn a1 n).coprime (pell.yn a1 n)

theorem pell.y_increasing {a : } (a1 : 1 < a) {m n : } :
m < npell.yn a1 m < pell.yn a1 n

theorem pell.x_increasing {a : } (a1 : 1 < a) {m n : } :
m < npell.xn a1 m < pell.xn a1 n

theorem pell.yn_ge_n {a : } (a1 : 1 < a) (n : ) :
n pell.yn a1 n

theorem pell.y_mul_dvd {a : } (a1 : 1 < a) (n k : ) :
pell.yn a1 n pell.yn a1 (n * k)

theorem pell.y_dvd_iff {a : } (a1 : 1 < a) (m n : ) :
pell.yn a1 m pell.yn a1 n m n

theorem pell.xy_modeq_yn {a : } (a1 : 1 < a) (n k : ) :
pell.xn a1 (n * k) pell.xn a1 n ^ k [MOD pell.yn a1 n ^ 2] pell.yn a1 (n * k) (k * pell.xn a1 n ^ (k - 1)) * pell.yn a1 n [MOD pell.yn a1 n ^ 3]

theorem pell.ysq_dvd_yy {a : } (a1 : 1 < a) (n : ) :
(pell.yn a1 n) * pell.yn a1 n pell.yn a1 (n * pell.yn a1 n)

theorem pell.dvd_of_ysq_dvd {a : } (a1 : 1 < a) {n t : } :
(pell.yn a1 n) * pell.yn a1 n pell.yn a1 tpell.yn a1 n t

theorem pell.pell_zd_succ_succ {a : } (a1 : 1 < a) (n : ) :
pell.pell_zd a1 (n + 2) + pell.pell_zd a1 n = (2 * a) * pell.pell_zd a1 (n + 1)

theorem pell.xy_succ_succ {a : } (a1 : 1 < a) (n : ) :
pell.xn a1 (n + 2) + pell.xn a1 n = (2 * a) * pell.xn a1 (n + 1) pell.yn a1 (n + 2) + pell.yn a1 n = (2 * a) * pell.yn a1 (n + 1)

theorem pell.xn_succ_succ {a : } (a1 : 1 < a) (n : ) :
pell.xn a1 (n + 2) + pell.xn a1 n = (2 * a) * pell.xn a1 (n + 1)

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)

theorem pell.xz_succ_succ {a : } (a1 : 1 < a) (n : ) :
pell.xz a1 (n + 2) = (2 * a) * pell.xz a1 (n + 1) - pell.xz a1 n

theorem pell.yz_succ_succ {a : } (a1 : 1 < a) (n : ) :
pell.yz a1 (n + 2) = (2 * a) * pell.yz a1 (n + 1) - pell.yz a1 n

theorem pell.yn_modeq_a_sub_one {a : } (a1 : 1 < a) (n : ) :
pell.yn a1 n n [MOD a - 1]

theorem pell.yn_modeq_two {a : } (a1 : 1 < a) (n : ) :
pell.yn a1 n n [MOD 2]

theorem pell.x_sub_y_dvd_pow_lem {a : } (a1 : 1 < a) (y2 y1 y0 yn1 yn0 xn1 xn0 ay a2 : ) :
(a2 * yn1 - yn0) * ay + y2 - (a2 * xn1 - xn0) = y2 - a2 * y1 + y0 + a2 * (yn1 * ay + y1 - xn1) - (yn0 * ay + y0 - xn0)

theorem pell.x_sub_y_dvd_pow {a : } (a1 : 1 < a) (y n : ) :
(2 * a) * y - (y) * y - 1 (pell.yz a1 n) * (a - y) + (y ^ n) - pell.xz a1 n

theorem pell.xn_modeq_x2n_add_lem {a : } (a1 : 1 < a) (n j : ) :
pell.xn a1 n ((d a1) * pell.yn a1 n) * (pell.yn a1 n) * pell.xn a1 j + pell.xn a1 j

theorem pell.xn_modeq_x2n_add {a : } (a1 : 1 < a) (n j : ) :
pell.xn a1 (2 * n + j) + pell.xn a1 j 0 [MOD pell.xn a1 n]

theorem pell.xn_modeq_x2n_sub_lem {a : } (a1 : 1 < a) {n j : } :
j npell.xn a1 (2 * n - j) + pell.xn a1 j 0 [MOD pell.xn a1 n]

theorem pell.xn_modeq_x2n_sub {a : } (a1 : 1 < a) {n j : } :
j 2 * npell.xn a1 (2 * n - j) + pell.xn a1 j 0 [MOD pell.xn a1 n]

theorem pell.xn_modeq_x4n_add {a : } (a1 : 1 < a) (n j : ) :
pell.xn a1 (4 * n + j) pell.xn a1 j [MOD pell.xn a1 n]

theorem pell.xn_modeq_x4n_sub {a : } (a1 : 1 < a) {n j : } :
j 2 * npell.xn a1 (4 * n - j) pell.xn a1 j [MOD pell.xn a1 n]

theorem pell.eq_of_xn_modeq_lem1 {a : } (a1 : 1 < a) {i n j : } :
i < jj < npell.xn a1 i % pell.xn a1 n < pell.xn a1 j % pell.xn a1 n

theorem pell.eq_of_xn_modeq_lem2 {a : } (a1 : 1 < a) {n : } :
2 * pell.xn a1 n = pell.xn a1 (n + 1)a = 2 n = 0

theorem pell.eq_of_xn_modeq_lem3 {a : } (a1 : 1 < a) {i n : } (npos : 0 < n) {j : } :
i < jj 2 * nj n¬(a = 2 n = 1 i = 0 j = 2)pell.xn a1 i % pell.xn a1 n < pell.xn a1 j % pell.xn a1 n

theorem pell.eq_of_xn_modeq_le {a : } (a1 : 1 < a) {i j n : } :
0 < ni jj 2 * npell.xn a1 i pell.xn a1 j [MOD pell.xn a1 n]¬(a = 2 n = 1 i = 0 j = 2)i = j

theorem pell.eq_of_xn_modeq {a : } (a1 : 1 < a) {i j n : } :
0 < ni 2 * nj 2 * npell.xn a1 i pell.xn a1 j [MOD pell.xn a1 n](a = 2n = 1(i = 0j 2) (i = 2j 0))i = j

theorem pell.eq_of_xn_modeq' {a : } (a1 : 1 < a) {i j n : } :
0 < ii nj 4 * npell.xn a1 j pell.xn a1 i [MOD pell.xn a1 n]j = i j + i = 4 * n

theorem pell.modeq_of_xn_modeq {a : } (a1 : 1 < a) {i j n : } :
0 < ii npell.xn a1 j pell.xn a1 i [MOD pell.xn a1 n]j i [MOD 4 * n] j + i 0 [MOD 4 * n]

theorem pell.xy_modeq_of_modeq {a b c : } (a1 : 1 < a) (b1 : 1 < b) (h : a b [MOD c]) (n : ) :
pell.xn a1 n pell.xn b1 n [MOD c] pell.yn a1 n pell.yn b1 n [MOD c]

theorem pell.matiyasevic {a k x y : } :
(∃ (a1 : 1 < a), pell.xn a1 k = x pell.yn a1 k = y) 1 < a k y (x = 1 y = 0 ∃ (u v s t b : ), x * x - ((a * a - 1) * y) * y = 1 u * u - ((a * a - 1) * v) * v = 1 s * s - ((b * b - 1) * t) * t = 1 1 < b b 1 [MOD 4 * y] b a [MOD u] 0 < v y * y v s x [MOD u] t k [MOD 4 * y])

theorem pell.eq_pow_of_pell_lem {a y k : } :
1 < a0 < y0 < ky ^ k < a(y ^ k) < (2 * a) * y - (y) * y - 1

theorem pell.eq_pow_of_pell {m n k : } :
n ^ k = m k = 0 m = 1 0 < k (n = 0 m = 0 0 < n ∃ (w a t z : ) (a1 : 1 < a), pell.xn a1 k (pell.yn a1 k) * (a - n) + m [MOD t] (2 * a) * n = t + (n * n + 1) m < t n w k w a * a - (((w + 1) * (w + 1) - 1) * w * z) * w * z = 1)