Lucas sequences

StructureParameters of a Lucas sequence#✓fully proved

Lucas sequence parameters are a pair of integers \((P, Q)\) with \(Q \ne 0\).

The condition \(Q \ne 0\) follows the convention of the sources.

structure LucasSequenceParams where
  p : ℤ
  q : ℤ
  q_ne_zero : q ≠ 0

Used by 198

DefinitionCoprime Lucas sequence parameters#✓fully proved

Lucas sequence parameters \((P, Q)\) are coprime when there exist integers \(x\) and \(y\) with \(xP + yQ = 1\).

This additional condition is imposed in some applications of Lucas sequences.

def LucasSequenceParams.IsCoprime (params : LucasSequenceParams) : Prop :=
  ∃ x y : ℤ, x * params.p + y * params.q = 1

Uses 1 · Used by 3

Statement usesParameters of a Lucas sequence

Used by\(D\)-Carmichael number · \(9\) is not a \(5\)-Carmichael number · \(D\)-Carmichael numbers are not prime

DefinitionLucas sequence \(U(P, Q)\)#✓fully proved

For Lucas sequence parameters \((P, Q)\), the Lucas sequence \(U(P, Q)\) is the integer sequence \((U_n)_{n \ge 0}\) with \(U_0 = 0\), \(U_1 = 1\) and \(U_{n+2} = P U_{n+1} - Q U_n\) for every natural number \(n\).

def lucasU (params : LucasSequenceParams) : ℕ → ℤ
  | 0 => 0
  | 1 => 1
  | n + 2 => params.p * lucasU params (n + 1) - params.q * lucasU params n

Uses 1 · Used by 154

Statement usesParameters of a Lucas sequence

DefinitionCompanion Lucas sequence \(V(P, Q)\)#✓fully proved

For Lucas sequence parameters \((P, Q)\), the companion Lucas sequence \(V(P, Q)\) is the integer sequence \((V_n)_{n \ge 0}\) with \(V_0 = 2\), \(V_1 = P\) and \(V_{n+2} = P V_{n+1} - Q V_n\) for every natural number \(n\).

def lucasV (params : LucasSequenceParams) : ℕ → ℤ
  | 0 => 2
  | 1 => params.p
  | n + 2 => params.p * lucasV params (n + 1) - params.q * lucasV params n

Uses 1 · Used by 55

Statement usesParameters of a Lucas sequence

Used bySanford's Lucas-sequence dilogarithm series for \(Q < 0\) · \(p\)-Lucas numbers as a companion Lucas sequence · Addition formula for the Lucas sequence \(U\) · Bounds on Lucas sequences by powers of the dominant root · The companion Lucas sequence in terms of the fundamental one · A quadratic equation in the companion Lucas sequence · Square of the companion Lucas sequence · Remainder bound for weighted Lucas power sums when \(y = 1\) · Reciprocal series of Lucas sequences with doubling subscripts · Dickson pseudoprimes · Dickson pseudoprimes of the second kind · Euler–Lucas pseudoprime · 9 is an Euler–Lucas pseudoprime for P = 1, Q = 5 · 9 is a Frobenius pseudoprime for P = 4, Q = -1 · Strong Lucas pseudoprimes · \(9\) is a strong Lucas pseudoprime for \((P, Q) = (1, 5)\) · Super strong Lucas pseudoprimes from composed Lucas pairs · Growth and positivity of Lucas sequences with positive discriminant · Divisibility of Lucas sequences at divisible indices · Lucas sequences under negation of the first parameter · Doubling formula \(U_{2n} = U_n V_n\) for Lucas sequences · \(P\) divides \(U_{2n}\), and \(V_n\) for odd \(n\) · Binet formulas for Lucas sequences · Binet formulas for Lucas sequences over any field · The Lucas sequence \(V(1, -1)\) gives the Lucas numbers · Addition formula \(2U_{m+n} = U_m V_n + V_m U_n\) for Lucas sequences · Doubling formulas and divisibility for Lucas sequences · Subsequences of a second-order linear recurrence · Even-index Catalan convolution with Lucas sequences · Shifted Catalan convolution with Lucas sequences · Binomial-Catalan sum with Lucas sequences · Alternating binomial-Catalan sum with Lucas sequences · Dixon-type alternating sum with Lucas sequences · Alternating sum of \(\binom{2n}{k} \binom{4n}{2k}\) with Lucas sequences · Alternating sum with reciprocal binomial coefficients and Lucas sequences · Sum of \(\binom{n}{k} \binom{2n}{n+k} \binom{n+k}{k}\) with Lucas sequences · Binomial sums with signs \((-1)^{\binom{k}{2}}\) and Lucas sequences · Squared-binomial convolution of the Lucas sequences U and V · Alternating squared-binomial sum with Lucas sequences · Alternating two-binomial Catalan convolution of U and V · Alternating triple-binomial convolution of U and V · Convolution of U and V with shifted binomial weights · Power-weighted Pell sums along odd multiples · Integral representation of the companion \(k\)-Jacobsthal numbers · Integral representation of the Jacobsthal-Lucas numbers along arithmetic progressions · Integral representation of the Jacobsthal-Lucas numbers at multiples of an index · Integral representation of Jacobsthal numbers with an offset · Integral representation of Jacobsthal numbers at multiples · Addition formulas for k-Jacobsthal numbers · Binet-type identities for k-Jacobsthal numbers · Integral representation of k-Jacobsthal numbers at multiples · Integral representation of even- and odd-indexed k-Jacobsthal–Lucas numbers · Integral representation of k-Jacobsthal–Lucas numbers at multiples · The \(k\)-Jacobsthal-Lucas number \(j_{k,2}\) · Companion \(k\)-Jacobsthal numbers via Lucas sequences

DefinitionFibonacci parameters for Lucas sequences#✓fully proved

The Fibonacci parameters are the Lucas sequence parameters \(P = 1\) and \(Q = -1\); they satisfy the required condition \(Q \ne 0\).

These parameters give the Fibonacci and classical Lucas-number sequences.

def fibonacciLucasParams : LucasSequenceParams where
  p := 1
  q := -1
  q_ne_zero := by decide

Uses 1 · Used by 5

Statement usesParameters of a Lucas sequence

Used byThe Lucas sequence \(U(1, -1)\) is the Fibonacci sequence · The Lucas sequence \(V(1, -1)\) gives the Lucas numbers · Period of the Fibonacci sequence modulo 2 · Restricted period of the Fibonacci sequence modulo 2 · \(9\) is not a \(5\)-Carmichael number

DefinitionLucas numbers#✓fully proved

The Lucas numbers are the natural numbers \(L_n\) defined by \(L_0 = 2\), \(L_1 = 1\) and \(L_{n+2} = L_{n+1} + L_n\) for every natural number \(n\). They begin \(2, 1, 3, 4, 7, \dots\).

def lucasNumber : ℕ → ℕ
  | 0 => 2
  | 1 => 1
  | n + 2 => lucasNumber (n + 1) + lucasNumber n

Used by 77

TheoremThe Lucas sequence \(U(1, -1)\) is the Fibonacci sequence#✓fully proved

For every natural number \(n\), the \(n\)-th term of the Lucas sequence \(U(1, -1)\) equals the Fibonacci number \(F_n\), where \(F_0 = 0\), \(F_1 = 1\) and \(F_{n+2} = F_{n+1} + F_n\).

theorem lucasU_fibonacciLucasParams (n : ℕ) :
    lucasU fibonacciLucasParams n = (Nat.fib n : ℤ)

def lucasU (params : LucasSequenceParams) : ℕ → ℤ
  | 0 => 0
  | 1 => 1
  | n + 2 => params.p * lucasU params (n + 1) - params.q * lucasU params n

MathlibExt/NumberTheory/LucasSequence.lean:50

def fibonacciLucasParams : LucasSequenceParams where
  p := 1
  q := -1
  q_ne_zero := by decide

MathlibExt/NumberTheory/LucasSequence.lean:63

Uses 3 · Used by 2

Statement usesFibonacci parameters for Lucas sequences · Lucas sequence \(U(P, Q)\)

Proof usesParameters of a Lucas sequence

Used byRestricted period of the Fibonacci sequence modulo 2 · \(9\) is not a \(5\)-Carmichael number

TheoremRecurrence for the Lucas sequence \(U(P, Q)\)#✓fully proved

For Lucas sequence parameters \((P, Q)\) and every natural number \(n\), the Lucas sequence \(U = U(P, Q)\) satisfies \(U_{n+2} = P U_{n+1} - Q U_n\).

theorem lucasU_add_two (params : LucasSequenceParams) (n : ℕ) :
    lucasU params (n + 2) =
      params.p * lucasU params (n + 1) - params.q * lucasU params n

structure LucasSequenceParams where
  p : ℤ
  q : ℤ
  q_ne_zero : q ≠ 0

MathlibExt/NumberTheory/LucasSequence.lean:39

def lucasU (params : LucasSequenceParams) : ℕ → ℤ
  | 0 => 0
  | 1 => 1
  | n + 2 => params.p * lucasU params (n + 1) - params.q * lucasU params n

MathlibExt/NumberTheory/LucasSequence.lean:50

Uses 2 · Used by 2

Statement usesParameters of a Lucas sequence · Lucas sequence \(U(P, Q)\)

Used byCassini's identity for Lucas sequences · The \(k\)-Jacobsthal numbers as companion numbers

TheoremCassini's identity for Lucas sequences#✓fully proved

For Lucas sequence parameters \((P, Q)\) and every natural number \(n\), the Lucas sequence \(U = U(P, Q)\) satisfies \(U_{n+1}^2 - U_n U_{n+2} = Q^n\).

theorem lucasU_cassini (params : LucasSequenceParams) (n : ℕ) :
    lucasU params (n + 1) ^ 2 - lucasU params n * lucasU params (n + 2) =
      params.q ^ n

structure LucasSequenceParams where
  p : ℤ
  q : ℤ
  q_ne_zero : q ≠ 0

MathlibExt/NumberTheory/LucasSequence.lean:39

def lucasU (params : LucasSequenceParams) : ℕ → ℤ
  | 0 => 0
  | 1 => 1
  | n + 2 => params.p * lucasU params (n + 1) - params.q * lucasU params n

MathlibExt/NumberTheory/LucasSequence.lean:50

Uses 3

Statement usesParameters of a Lucas sequence · Lucas sequence \(U(P, Q)\)

Proof usesRecurrence for the Lucas sequence \(U(P, Q)\)

TheoremThe Lucas sequence \(V(1, -1)\) gives the Lucas numbers#✓fully proved

For every natural number \(n\), the \(n\)-th term of the companion Lucas sequence \(V(1, -1)\) equals the \(n\)-th Lucas number \(L_n\).

theorem lucasV_fibonacciLucasParams (n : ℕ) :
    lucasV fibonacciLucasParams n = (lucasNumber n : ℤ)

def lucasV (params : LucasSequenceParams) : ℕ → ℤ
  | 0 => 2
  | 1 => params.p
  | n + 2 => params.p * lucasV params (n + 1) - params.q * lucasV params n

MathlibExt/NumberTheory/LucasSequence.lean:56

def fibonacciLucasParams : LucasSequenceParams where
  p := 1
  q := -1
  q_ne_zero := by decide

MathlibExt/NumberTheory/LucasSequence.lean:63

def lucasNumber : ℕ → ℕ
  | 0 => 2
  | 1 => 1
  | n + 2 => lucasNumber (n + 1) + lucasNumber n

MathlibExt/NumberTheory/LucasSequence.lean:69

Uses 4

Statement usesFibonacci parameters for Lucas sequences · Lucas numbers · Companion Lucas sequence \(V(P, Q)\)

Proof usesParameters of a Lucas sequence

DefinitionSpecial primes of a Lucas pair#✓fully proved

For integers \(P\) and \(Q\), a natural number \(p\) is a special prime for the Lucas parameters \((P, Q)\) if \(p\) is prime and \(p\) divides \(\gcd(P, Q)\).

def IsLucasSpecialPrime (P Q : Int) (p : Nat) : Prop :=
  Nat.Prime p ∧ p ∣ Int.gcd P Q

Used by 1

Used bySpecial primes are the common prime divisors of the parameters

TheoremSpecial primes are the common prime divisors of the parameters#✓fully proved

For integers \(P\) and \(Q\) and a natural number \(p\), \(p\) is a special prime for the Lucas parameters \((P, Q)\) if and only if \(p\) is prime and \(p\) divides both \(P\) and \(Q\) in \(\mathbb{Z}\).

theorem isLucasSpecialPrime_iff (P Q : Int) (p : Nat) :
    IsLucasSpecialPrime P Q p ↔ Nat.Prime p ∧ (p : Int) ∣ P ∧ (p : Int) ∣ Q

Uses 1

Statement usesSpecial primes of a Lucas pair

TheoremBinet formulas for Lucas sequences over any field#✓fully proved

Let \(P\) and \(Q\) be integers with \(Q \ne 0\), let \(U_n = U_n(P, Q)\) and \(V_n = V_n(P, Q)\) be the associated Lucas sequences, and let \(\alpha\) and \(\beta\) be elements of a field \(K\) with \(\alpha + \beta = P\) and \(\alpha \beta = Q\) in \(K\). If \(\alpha \ne \beta\), then for every natural number \(n\), \(U_n = (\alpha^n - \beta^n) / (\alpha - \beta)\) and \(V_n = \alpha^n + \beta^n\) in \(K\). If \(\beta = \alpha\), then for every natural number \(n\), \(U_n = n \alpha^{n-1}\) and \(V_n = 2 \alpha^n\) in \(K\), where \(\alpha^{n-1}\) is read as \(1\) when \(n = 0\). Here the integers \(U_n\), \(V_n\), \(P\), \(Q\) and \(n\) are mapped into \(K\).

No assumption on the characteristic of \(K\) is made; for example \(K\) may be \(\mathbb{Z}/p\mathbb{Z}\) for a prime \(p\), where the coefficient \(n\) of the double-root formula is read modulo \(p\).

theorem lucas_binet_formulas_of_field
    {K : Type*} [Field K]
    (params : LucasSequenceParams) (alpha beta : K)
    (hsum : alpha + beta = (params.p : K))
    (hprod : alpha * beta = (params.q : K)) :
    (alpha ≠ beta → ∀ n : ℕ,
      (lucasU params n : K) = (alpha ^ n - beta ^ n) / (alpha - beta) ∧
      (lucasV params n : K) = alpha ^ n + beta ^ n) ∧
    (beta = alpha → ∀ n : ℕ,
      (lucasU params n : K) = (n : K) * alpha ^ (n - 1) ∧
      (lucasV params n : K) = 2 * alpha ^ n)

structure LucasSequenceParams where
  p : ℤ
  q : ℤ
  q_ne_zero : q ≠ 0

MathlibExt/NumberTheory/LucasSequence.lean:39

def lucasU (params : LucasSequenceParams) : ℕ → ℤ
  | 0 => 0
  | 1 => 1
  | n + 2 => params.p * lucasU params (n + 1) - params.q * lucasU params n

MathlibExt/NumberTheory/LucasSequence.lean:50

def lucasV (params : LucasSequenceParams) : ℕ → ℤ
  | 0 => 2
  | 1 => params.p
  | n + 2 => params.p * lucasV params (n + 1) - params.q * lucasV params n

MathlibExt/NumberTheory/LucasSequence.lean:56

Uses 3 · Used by 1

Statement usesParameters of a Lucas sequence · Lucas sequence \(U(P, Q)\) · Companion Lucas sequence \(V(P, Q)\)

Used byBinet formulas for Lucas sequences

TheoremBinet formulas for Lucas sequences#✓fully proved

Let \(P\) and \(Q\) be integers with \(Q \ne 0\), let \(U_n = U_n(P, Q)\) and \(V_n = V_n(P, Q)\) be the associated Lucas sequences, and let \(\alpha\) and \(\beta\) be elements of a field \(K\) of characteristic zero with \(\alpha + \beta = P\) and \(\alpha \beta = Q\) in \(K\). If \(\alpha \ne \beta\), then for every natural number \(n\), \(U_n = (\alpha^n - \beta^n) / (\alpha - \beta)\) and \(V_n = \alpha^n + \beta^n\) in \(K\). If \(\beta = \alpha\), then for every natural number \(n\), \(U_n = n \alpha^{n-1}\) and \(V_n = 2 \alpha^n\) in \(K\), where \(\alpha^{n-1}\) is read as \(1\) when \(n = 0\). Here the integers \(U_n\), \(V_n\), \(P\), \(Q\) and \(n\) are mapped into \(K\).

In the double-root case the hypotheses give \(P = 2 \alpha\) and \(Q = \alpha^2\).

theorem lucas_binet_formulas
    {K : Type*} [Field K] [CharZero K]
    (params : LucasSequenceParams) (alpha beta : K)
    (hsum : alpha + beta = (params.p : K))
    (hprod : alpha * beta = (params.q : K)) :
    (alpha ≠ beta → ∀ n : ℕ,
      (lucasU params n : K) = (alpha ^ n - beta ^ n) / (alpha - beta) ∧
      (lucasV params n : K) = alpha ^ n + beta ^ n) ∧
    (beta = alpha → ∀ n : ℕ,
      (lucasU params n : K) = (n : K) * alpha ^ (n - 1) ∧
      (lucasV params n : K) = 2 * alpha ^ n)

structure LucasSequenceParams where
  p : ℤ
  q : ℤ
  q_ne_zero : q ≠ 0

MathlibExt/NumberTheory/LucasSequence.lean:39

def lucasU (params : LucasSequenceParams) : ℕ → ℤ
  | 0 => 0
  | 1 => 1
  | n + 2 => params.p * lucasU params (n + 1) - params.q * lucasU params n

MathlibExt/NumberTheory/LucasSequence.lean:50

def lucasV (params : LucasSequenceParams) : ℕ → ℤ
  | 0 => 2
  | 1 => params.p
  | n + 2 => params.p * lucasV params (n + 1) - params.q * lucasV params n

MathlibExt/NumberTheory/LucasSequence.lean:56

Sources

Christian Ballot, "A Further Generalization of a Congruence of Wolstenholme", Journal of Integer Sequences 15 (2012), Article 12.8.6, sequence definitions and formulas at lines 274–289, https://cs.uwaterloo.ca/journals/JIS/VOL15/Ballot/ballot4.tex

Uses 4

Statement usesParameters of a Lucas sequence · Lucas sequence \(U(P, Q)\) · Companion Lucas sequence \(V(P, Q)\)

Proof usesBinet formulas for Lucas sequences over any field

DefinitionLucas sequence of the first kind#✓fully proved

For integers \(P\) and \(Q\), a sequence of integers \((u_n)_{n \ge 0}\) is the Lucas sequence of the first kind with parameters \(P\) and \(Q\) when \(u_0 = 0\), \(u_1 = 1\), and \(u_{n+2} = P u_{n+1} - Q u_n\) for every natural number \(n\).

public def IsLucasSequenceFirstKind (P Q : ℤ) (u : ℕ → ℤ) : Prop :=
  u 0 = 0 ∧ u 1 = 1 ∧ ∀ n : ℕ, u (n + 2) = P * u (n + 1) - Q * u n

Sources

https://cs.uwaterloo.ca/journals/JIS/VOL13/Smyth/smyth2.tex, lines 114-122.

Used by 5

Used byClassification of degenerate Lucas sequences · Lucas sequence of the first kind: value at one · Lucas sequence of the first kind: value at zero · Lucas sequence of the first kind: the recurrence · Integrality of generalized Lucasnomial Fuss–Catalan numbers

TheoremLucas sequence of the first kind: value at zero#✓fully proved

If \((u_n)_{n \ge 0}\) is the Lucas sequence of the first kind with integer parameters \(P\) and \(Q\), then \(u_0 = 0\).

public theorem IsLucasSequenceFirstKind.initialZero {P Q : ℤ} {u : ℕ → ℤ}
    (h : IsLucasSequenceFirstKind P Q u) : u 0 = 0

public def IsLucasSequenceFirstKind (P Q : ℤ) (u : ℕ → ℤ) : Prop :=
  u 0 = 0 ∧ u 1 = 1 ∧ ∀ n : ℕ, u (n + 2) = P * u (n + 1) - Q * u n

MathlibExt/NumberTheory/Recurrences/LucasSequenceFirstKind.lean:44

Uses 1 · Used by 1

Statement usesLucas sequence of the first kind

Used byIntegrality of generalized Lucasnomial Fuss–Catalan numbers

TheoremLucas sequence of the first kind: value at one#✓fully proved

If \((u_n)_{n \ge 0}\) is the Lucas sequence of the first kind with integer parameters \(P\) and \(Q\), then \(u_1 = 1\).

public theorem IsLucasSequenceFirstKind.initialOne {P Q : ℤ} {u : ℕ → ℤ}
    (h : IsLucasSequenceFirstKind P Q u) : u 1 = 1

public def IsLucasSequenceFirstKind (P Q : ℤ) (u : ℕ → ℤ) : Prop :=
  u 0 = 0 ∧ u 1 = 1 ∧ ∀ n : ℕ, u (n + 2) = P * u (n + 1) - Q * u n

MathlibExt/NumberTheory/Recurrences/LucasSequenceFirstKind.lean:44

Uses 1 · Used by 1

Statement usesLucas sequence of the first kind

Used byIntegrality of generalized Lucasnomial Fuss–Catalan numbers

TheoremLucas sequence of the first kind: the recurrence#✓fully proved

If \((u_n)_{n \ge 0}\) is the Lucas sequence of the first kind with integer parameters \(P\) and \(Q\), then \(u_{n+2} = P u_{n+1} - Q u_n\) for every natural number \(n\).

public theorem IsLucasSequenceFirstKind.recurrenceStep {P Q : ℤ} {u : ℕ → ℤ}
    (h : IsLucasSequenceFirstKind P Q u) (n : ℕ) :
    u (n + 2) = P * u (n + 1) - Q * u n

public def IsLucasSequenceFirstKind (P Q : ℤ) (u : ℕ → ℤ) : Prop :=
  u 0 = 0 ∧ u 1 = 1 ∧ ∀ n : ℕ, u (n + 2) = P * u (n + 1) - Q * u n

MathlibExt/NumberTheory/Recurrences/LucasSequenceFirstKind.lean:44

Uses 1 · Used by 1

Statement usesLucas sequence of the first kind

Used byIntegrality of generalized Lucasnomial Fuss–Catalan numbers

DefinitionNondegenerate Lucas pair#✓fully proved

A pair of integers \((P, Q)\) is nondegenerate when \(Q \ne 0\) and, for all complex numbers \(\alpha\) and \(\beta\) with \(\alpha + \beta = P\) and \(\alpha \beta = Q\), the quotient \(\alpha / \beta\) is not a root of unity. Such \(\alpha\) and \(\beta\) are the two roots of \(x^2 - P x + Q\), in either order.

public def IsNondegenerateLucasPair (P Q : ℤ) : Prop :=
  Q ≠ 0 ∧ ∀ α β : ℂ, α + β = (P : ℂ) → α * β = (Q : ℂ) → ¬ IsOfFinOrder (α / β)

Sources

https://cs.uwaterloo.ca/journals/JIS/VOL13/Smyth/smyth2.tex: lines 621-622 say a Lucas sequence is degenerate iff Q = 0 or α / β is a root of unity, where α and β are the two roots of x² - P x + Q. Lines 114-122 establish α + β = P and α * β = Q.

Used by 50

Used byCarmichael's primitive divisor theorem · Bilu–Hanrot–Voutier theorem for Lucas sequences · Rotkiewicz: Frobenius pseudoprimes in arithmetic progressions · Frobenius and non-Frobenius pseudoprimes of the form \(U_{2m}/P\) · Rotkiewicz: strong Lucas and Frobenius pseudoprimes with two prime factors · From Euler–Lucas to Frobenius pseudoprimes · From strong Lucas to Frobenius pseudoprimes when Q = ±1 · Lucas pseudoprimes from even-index Lucas terms divided by P · Strong Lucas pseudoprimes via the \(2\)-adic valuation of ranks · Strong Lucas pseudoprimes among the terms \(|U_m|\) · Lucas pseudoprimes of odd rank are strong · Composite terms \(|U_p|\) are super strong Lucas pseudoprimes · Super strong Lucas pseudoprimes from composed Lucas pairs · Super Lucas pseudoprimes of the form \(|U_{2p}/P|\) · Super strong Lucas pseudoprimes from equal ranks of appearance · Rank of appearance and super Lucas pseudoprimes · \(|U_m|\) is a strong Lucas and Frobenius pseudoprime when \(Q = \pm 1\) · When \(|U_{2m}/P|\) is a Frobenius pseudoprime, for \(Q = \pm 1\) · \(|U_{2m}/P|\) is a Lucas pseudoprime when \(Q = \pm 1\) · Compositeness criteria for \(|U_p|\) · Lucas-type pseudoprime properties are unchanged by \(P \mapsto -P\) · Least multiples in \(S(U)\) for nondegenerate \(U(P, Q)\) · Multiples of \(4\) in the average set when \(P \equiv 0\) and \(Q \equiv 1\) · Odd moduli in the average set when \(P \equiv 2\) and \(Q \equiv 1\) · Multiples of \(6\) in the average set when \(P \equiv 1\) and \(Q \equiv 1\) · Multiples of \(3\) in the average set when \(P \equiv -1\) and \(Q \equiv 1\) · Period and average sets when \(P = -Q - 1\) · Period and average sets when \(P = Q + 1\) · Powers of two when \(P \equiv 2\) and \(-Q \equiv 1 \pmod 4\) · Powers of two when \(P \equiv 0\) and \(-Q \equiv -1 \pmod 4\) · Period set equals index-divisible set for nondegenerate \(U(P, Q)\) with \(P = Q + 1\) · Least multiples of \(2^k n_1\) in the period set for even \(P\) · Least period and average multiples for \(Q = -1\) · Least period and average multiples for \(Q = 1\) · Lucas sums not divisible by \(2^k\) when \(P \equiv 2\) and \(-Q \equiv -1 \pmod 4\) · Lucas sums not divisible by \(2^k\) when \(P \equiv 0\) and \(-Q \equiv 1 \pmod 4\) · Lucas sums and powers of two for even \(P\) and odd \(Q\) · Prime-power divisibility of Lucas sums · Uniform distribution of Lucas sequences modulo primes dividing the discriminant · Wyler's theorem on the period of a Lucas sequence · Lucas sequences with \(P = Q + 1\) · Lucas sequences with \(P = -Q - 1\) · Period and restricted period of Lucas sequences with \(Q = -1\) · Period and restricted period of Lucas sequences with \(Q = 1\) · Periods of a Lucas sequence modulo a prime · Period quotients and seeds of \(S(U)\) · Integral averages for \(U(P, 1)\) · Smyth's description of the indices \(n\) with \(n \mid U_n\) · Members of \(S(U)\) of the form \(2^i 3^j\) · Non-integer period average of a Lucas sequence when \(\gcd(n, a, b) > 1\)

TheoremAddition formula \(2U_{m+n} = U_m V_n + V_m U_n\) for Lucas sequences#●ready to prove

For all integers \(P\) and \(Q\) with \(Q \neq 0\) and all natural numbers \(m\) and \(n\), the Lucas sequences \(U_n = U_n(P, Q)\) and \(V_n = V_n(P, Q)\) satisfy \(2U_{m+n} = U_m V_n + V_m U_n\).

This is the integer specialization of the paper's Proposition 1: its generalized Fibonacci numbers \(F_n\) and Lucas numbers \(L_n\), with recurrence \(x_{n+2} = a x_{n+1} + b x_n\), are \(U_n(a, -b)\) and \(V_n(a, -b)\), and the paper allows real \(a\) and \(b\).

theorem_wanted two_mul_lucasU_add
    (params : MetaMathlibExt.LucasSequenceParams) (m n : ℕ) :
    2 * MetaMathlibExt.lucasU params (m + n) =
      MetaMathlibExt.lucasU params m * MetaMathlibExt.lucasV params n +
        MetaMathlibExt.lucasV params m * MetaMathlibExt.lucasU params n

structure LucasSequenceParams where
  p : ℤ
  q : ℤ
  q_ne_zero : q ≠ 0

MathlibExt/NumberTheory/LucasSequence.lean:39

def lucasU (params : LucasSequenceParams) : ℕ → ℤ
  | 0 => 0
  | 1 => 1
  | n + 2 => params.p * lucasU params (n + 1) - params.q * lucasU params n

MathlibExt/NumberTheory/LucasSequence.lean:50

def lucasV (params : LucasSequenceParams) : ℕ → ℤ
  | 0 => 2
  | 1 => params.p
  | n + 2 => params.p * lucasV params (n + 1) - params.q * lucasV params n

MathlibExt/NumberTheory/LucasSequence.lean:56

Sources

Vladimir V. Kruchinin and Maria Y. Perminova, "Identities and Hadamard Product of the Generalized Fibonacci, Lucas, Catalan, and Harmonic Numbers", Proposition 1.

Uses 3

Statement usesParameters of a Lucas sequence · Lucas sequence \(U(P, Q)\) · Companion Lucas sequence \(V(P, Q)\)

19 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.