mathlib documentation

number_theory.pell

@[simp]

theorem pell.d_pos {a : ℕ} (a1 : 1 < a) :

0 < d a1

@[nolint]

def pell.pell {a : ℕ} (a1 : 1 < a) (a_1 : ℕ) :

The Pell sequences, defined together in mutual recursion.

Equations

pell.pell a1 = λ (n : ℕ), n.rec_on (1, 0) (λ (n : ℕ) (xy : ℕ × ℕ), ((xy.fst) * a + (d a1) * xy.snd, xy.fst + (xy.snd) * a))

def pell.xn {a : ℕ} (a1 : 1 < a) (n : ℕ) :

The Pell x sequence.

Equations

pell.xn a1 n = (pell.pell a1 n).fst

def pell.yn {a : ℕ} (a1 : 1 < a) (n : ℕ) :

The Pell y sequence.

Equations

pell.yn a1 n = (pell.pell a1 n).snd

@[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 : ℕ} (a1 : 1 < a) (n : ℕ) :

Equations

pell.xz a1 n = ↑(pell.xn a1 n)

def pell.yz {a : ℕ} (a1 : 1 < a) (n : ℕ) :

Equations

pell.yz a1 n = ↑(pell.yn a1 n)

def pell.az {a : ℕ} (a1 : 1 < a) :

Equations

pell.az a1 = ↑a

theorem pell.asq_pos {a : ℕ} (a1 : 1 < a) :

0 < 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) (n : ℕ) :

ℤ√↑(d a1)

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

Equations

pell.pell_zd a1 n = {re := ↑(pell.xn a1 n), im := ↑(pell.yn a1 n)}

@[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) (a_1 : ℤ√↑(d a1)) :

Prop

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

Equations

pell.is_pell a1 {re := x, im := y} = (x * x - ((↑(d a1)) * y) * y = 1)

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)} (hb : pell.is_pell a1 b) (hc : pell.is_pell a1 c) :

pell.is_pell a1 (b * c)

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

pell.is_pell a1 b ↔ pell.is_pell a1 b.conj

@[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 : ℕ) :

pell.is_pell a1 (pell.pell_zd a1 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) :

zsqrtd.nonsquare (d a1)

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)) (a_1 : 1 ≤ b) (a_2 : pell.is_pell a1 b) (a_3 : b ≤ pell.pell_zd a1 n) :

∃ (n : ℕ), b = pell.pell_zd a1 n

theorem pell.eq_pell_zd {a : ℕ} (a1 : 1 < a) (b : ℤ√↑(d a1)) (b1 : 1 ≤ b) (hp : pell.is_pell a1 b) :

∃ (n : ℕ), b = pell.pell_zd a1 n

theorem pell.eq_pell {a : ℕ} (a1 : 1 < a) {x y : ℕ} (hp : 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 : ℕ} (h : n ≤ m) :

pell.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 : ℕ} (h : n ≤ m) :

pell.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 : ℕ} (h : n ≤ m) :

pell.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 : ℕ} (a_1 : m < n) :

pell.yn a1 m < pell.yn a1 n

theorem pell.x_increasing {a : ℕ} (a1 : 1 < a) {m n : ℕ} (a_1 : m < n) :

pell.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 : ℕ} (h : (pell.yn a1 n) * pell.yn a1 n ∣ pell.yn a1 t) :

pell.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 : ℕ} (h : j ≤ n) :

pell.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 : ℕ} (h : j ≤ 2 * n) :

pell.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 : ℕ} (h : j ≤ 2 * n) :

pell.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 : ℕ} (a_1 : i < j) (a_2 : j < n) :

pell.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 : ℕ} (h : 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 : ℕ} (a_1 : i < j) (a_2 : j ≤ 2 * n) (a_3 : j ≠ n) (a_4 : ¬(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 : ℕ} (npos : 0 < n) (ij : i ≤ j) (j2n : j ≤ 2 * n) (h : pell.xn a1 i ≡ pell.xn a1 j [MOD pell.xn a1 n]) (ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)) :

i = j

theorem pell.eq_of_xn_modeq {a : ℕ} (a1 : 1 < a) {i j n : ℕ} (npos : 0 < n) (i2n : i ≤ 2 * n) (j2n : j ≤ 2 * n) (h : pell.xn a1 i ≡ pell.xn a1 j [MOD pell.xn a1 n]) (ntriv : a = 2 → n = 1 → (i = 0 → j ≠ 2) ∧ (i = 2 → j ≠ 0)) :

i = j

theorem pell.eq_of_xn_modeq' {a : ℕ} (a1 : 1 < a) {i j n : ℕ} (ipos : 0 < i) (hin : i ≤ n) (j4n : j ≤ 4 * n) (h : pell.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 : ℕ} (ipos : 0 < i) (hin : i ≤ n) (h : pell.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 : ℕ} (a1 : 1 < a) (ypos : 0 < y) (a_1 : 0 < k) (a_2 : y ^ 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)