Oresme numbers

TheoremSelf-convolution of the Oresme numbers#●ready to prove

Let \(O_m = m/2^m\) denote the Oresme numbers. For every natural number \(n\), \(\sum_{k=0}^{n} O_k O_{n-k} = \frac{(n+1) n (n-1)}{6 \cdot 2^n}\).

public theorem_wanted oresme_convolution_self (n : ℕ) :
    ∑ k ∈ Finset.range (n + 1), ((k : ℚ) / 2 ^ k) * (((n - k : ℕ) : ℚ) / 2 ^ (n - k)) =
      ((n : ℚ) + 1) * n * ((n : ℚ) - 1) / (6 * 2 ^ n)

Sources

• Michael R. Bacon and Charles K. Cook, Some Properties of Oresme Numbers and Convolutions with Various Second Order Sequences, The Fibonacci Quarterly 62 (2024), no. 3, Article cookbacon061124, Proposition 2.1.

TheoremFibonacci–Oresme convolution#●ready to prove

Let \(F_m\) denote the Fibonacci numbers, with \(F_0 = 0\), \(F_1 = 1\) and \(F_{m+2} = F_{m+1} + F_m\), and let \(O_m = m/2^m\) denote the Oresme numbers. For every natural number \(n\), \(\sum_{k=0}^{n} F_k O_{n-k} = \frac{2}{5} F_{n+1} - \frac{2(n+1)}{5 \cdot 2^n}\).

public theorem_wanted fib_oresme_convolution (n : ℕ) :
    ∑ k ∈ Finset.range (n + 1), (Nat.fib k : ℚ) * (((n - k : ℕ) : ℚ) / 2 ^ (n - k)) =
      2 / 5 * (Nat.fib (n + 1) : ℚ) - 2 * ((n : ℚ) + 1) / (5 * 2 ^ n)

Sources

• Michael R. Bacon and Charles K. Cook, Some Properties of Oresme Numbers and Convolutions with Various Second Order Sequences, The Fibonacci Quarterly 62 (2024), no. 3, Article cookbacon061124, Proposition 4.1.

TheoremOresme–Fibonacci congruence modulo 5#●ready to prove

Let \(F_n\) denote the Fibonacci numbers, with \(F_0 = 0\) and \(F_1 = 1\). For every natural number \(n\), \(2^{n-1} F_n \equiv n \pmod 5\), where at \(n = 0\) the exponent \(n - 1\) is taken to be \(0\) (both sides are then \(0\)).

public theorem_wanted two_pow_pred_mul_fib_modEq_five (n : ℕ) :
    2 ^ (n - 1) * Nat.fib n ≡ n [MOD 5]

Sources

• Michael R. Bacon and Charles K. Cook, Some Properties of Oresme Numbers and Convolutions with Various Second Order Sequences, The Fibonacci Quarterly 62 (2024), no. 3, Article cookbacon061124, Corollary 4.2.

TheoremLucas–Oresme convolution#●ready to prove

Let \(L_m\) denote the Lucas numbers and let \(O_m = m/2^m\) denote the Oresme numbers. For every natural number \(n\), \(\sum_{k=0}^{n} L_k O_{n-k} = \frac{2}{5} L_{n+1} - \frac{2}{5 \cdot 2^n}\).

public theorem_wanted lucasNumber_oresme_convolution (n : ℕ) :
    ∑ k ∈ Finset.range (n + 1), (lucasNumber k : ℚ) * (((n - k : ℕ) : ℚ) / 2 ^ (n - k)) =
      2 / 5 * (lucasNumber (n + 1) : ℚ) - 2 / (5 * 2 ^ n)

Sources

• Michael R. Bacon and Charles K. Cook, Some Properties of Oresme Numbers and Convolutions with Various Second Order Sequences, The Fibonacci Quarterly 62 (2024), no. 3, Article cookbacon061124, Proposition 4.3.

Uses 1

Statement usesLucas numbers

TheoremPowers of two times Lucas numbers modulo 5#●ready to prove

Let \(L_m\) denote the Lucas numbers. For every natural number \(n\), \(2^n L_{n+1} \equiv 1 \pmod{5}\).

public theorem_wanted two_pow_mul_lucasNumber_succ_modEq_five (n : ℕ) :
    2 ^ n * lucasNumber (n + 1) ≡ 1 [MOD 5]

Sources

• Michael R. Bacon and Charles K. Cook, Some Properties of Oresme Numbers and Convolutions with Various Second Order Sequences, The Fibonacci Quarterly 62 (2024), no. 3, Article cookbacon061124, Corollary 4.4.

Uses 1

Statement usesLucas numbers

TheoremPell–Oresme convolution#●ready to prove

Let \(P_m\) denote the Pell numbers and let \(O_m = m/2^m\) denote the Oresme numbers. For every natural number \(n\), \(\sum_{k=0}^{n} P_k O_{n-k} = \frac{2}{49}(5 P_{n+1} - 4 P_n) - \frac{2(7n + 5)}{49 \cdot 2^n}\).

public theorem_wanted pellNumber_oresme_convolution (n : ℕ) :
    ∑ k ∈ Finset.range (n + 1), (pellNumber k : ℚ) * (((n - k : ℕ) : ℚ) / 2 ^ (n - k)) =
      2 / 49 * (5 * (pellNumber (n + 1) : ℚ) - 4 * pellNumber n) -
        2 / 49 * ((7 * (n : ℚ) + 5) / 2 ^ n)

Sources

• Michael R. Bacon and Charles K. Cook, Some Properties of Oresme Numbers and Convolutions with Various Second Order Sequences, The Fibonacci Quarterly 62 (2024), no. 3, Article cookbacon061124, Proposition 5.2.

Uses 1

Statement usesPell numbers

TheoremOresme–Pell congruence modulo 49#●ready to prove

For every natural number \(n\), the Pell numbers \(P_n\) satisfy \(2^n (5 P_{n+1} - 4 P_n) \equiv 7n + 5 \pmod{49}\) as integers.

public theorem_wanted two_pow_mul_pellNumber_combination_modEq (n : ℕ) :
    2 ^ n * (5 * (pellNumber (n + 1) : ℤ) - 4 * pellNumber n) ≡ 7 * n + 5 [ZMOD 49]

Sources

• Michael R. Bacon and Charles K. Cook, Some Properties of Oresme Numbers and Convolutions with Various Second Order Sequences, The Fibonacci Quarterly 62 (2024), no. 3, Article cookbacon061124, Corollary 5.3.

Uses 1

Statement usesPell numbers

TheoremPell–Lucas–Oresme convolution#●ready to prove

Let \(Q_m\) denote the Pell–Lucas numbers, with \(Q_0 = Q_1 = 1\) and \(Q_{m+2} = 2Q_{m+1} + Q_m\), and let \(O_m = m/2^m\) denote the Oresme numbers. For every natural number \(n\), \(\sum_{k=0}^{n} Q_k O_{n-k} = \frac{2}{49}(5 Q_{n+1} - 4 Q_n) + \frac{7n - 2}{49 \cdot 2^n}\).

public theorem_wanted pellLucasSequence_oresme_convolution (n : ℕ) :
    ∑ k ∈ Finset.range (n + 1),
        (pellLucasSequence k : ℚ) * (((n - k : ℕ) : ℚ) / 2 ^ (n - k)) =
      2 / 49 * (5 * (pellLucasSequence (n + 1) : ℚ) - 4 * pellLucasSequence n) +
        1 / 49 * ((7 * (n : ℚ) - 2) / 2 ^ n)

Sources

• Michael R. Bacon and Charles K. Cook, Some Properties of Oresme Numbers and Convolutions with Various Second Order Sequences, The Fibonacci Quarterly 62 (2024), no. 3, Article cookbacon061124, Proposition 5.4.

Uses 1

Statement usesPell–Lucas sequence

TheoremOresme–Pell–Lucas congruence modulo 49#●ready to prove

Let \(Q_n\) denote the Pell–Lucas numbers, with \(Q_0 = Q_1 = 1\). For every natural number \(n\), \(2^{n+1} (5 Q_{n+1} - 4 Q_n) \equiv 2 - 7n \pmod{49}\) as integers.

The paper prints \(2^{n+1}(5Q_{n+1} - 4Q_n) \equiv 2 - 7n \equiv 0\). Its proof (base values \(2\) and \(44\) on both sides, inductive hypothesis \(2^{n+1}(5Q_{n+1} - 4Q_n) - (2 - 7n) \equiv 0\)) establishes the single congruence above, while the second link \(2 - 7n \equiv 0 \pmod{49}\) fails at \(n = 0\).

public theorem_wanted two_pow_succ_mul_pellLucasSequence_combination_modEq (n : ℕ) :
    2 ^ (n + 1) * (5 * (pellLucasSequence (n + 1) : ℤ) - 4 * pellLucasSequence n) ≡
      2 - 7 * n [ZMOD 49]

Sources

• Michael R. Bacon and Charles K. Cook, Some Properties of Oresme Numbers and Convolutions with Various Second Order Sequences, The Fibonacci Quarterly 62 (2024), no. 3, Article cookbacon061124, Corollary 5.5.

Uses 1

Statement usesPell–Lucas sequence

TheoremJacobsthal–Oresme convolution#●ready to prove

Let \(J_m\) denote the Jacobsthal numbers, the terms of the Lucas sequence \(U(1, -2)\), and let \(O_m = m/2^m\) denote the Oresme numbers. For every natural number \(n\), \(\sum_{k=0}^{n} J_k O_{n-k} = \frac{2}{9} J_{n+1} - \frac{2(n+1)}{9 \cdot 2^n}\).

public theorem_wanted jacobsthal_oresme_convolution (n : ℕ) :
    ∑ k ∈ Finset.range (n + 1),
        (lucasU ⟨1, -2, by decide⟩ k : ℚ) * (((n - k : ℕ) : ℚ) / 2 ^ (n - k)) =
      2 / 9 * (lucasU ⟨1, -2, by decide⟩ (n + 1) : ℚ) - 2 * ((n : ℚ) + 1) / (9 * 2 ^ n)

Sources

• Michael R. Bacon and Charles K. Cook, Some Properties of Oresme Numbers and Convolutions with Various Second Order Sequences, The Fibonacci Quarterly 62 (2024), no. 3, Article cookbacon061124, Proposition 6.2.

Uses 2

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

TheoremPowers of two times Jacobsthal numbers modulo 9#●ready to prove

Let \(J_m\) denote the Jacobsthal numbers, the terms of the Lucas sequence \(U(1, -2)\). For every natural number \(n\), \(2^n J_{n+1} \equiv n + 1 \pmod{9}\).

public theorem_wanted two_pow_mul_jacobsthal_succ_modEq_nine (n : ℕ) :
    2 ^ n * lucasU ⟨1, -2, by decide⟩ (n + 1) ≡ n + 1 [ZMOD 9]

Sources

• Michael R. Bacon and Charles K. Cook, Some Properties of Oresme Numbers and Convolutions with Various Second Order Sequences, The Fibonacci Quarterly 62 (2024), no. 3, Article cookbacon061124, Corollary 6.3.

Uses 2

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

TheoremJacobsthal–Lucas–Oresme convolution#●ready to prove

Let \(j_m\) denote the Jacobsthal–Lucas numbers and let \(O_m = m/2^m\) denote the Oresme numbers. For every natural number \(n\), \(\sum_{k=0}^{n} j_k O_{n-k} = \frac{2}{9} j_{n+1} - \frac{2}{9 \cdot 2^n}\).

The paper prints \(+\) where the equality sign belongs, with no relation between the two sides; this is the equality reading, which matches Propositions 4.3 and 6.2 and Corollary 6.5.

public theorem_wanted jacobsthalLucasNumber_oresme_convolution (n : ℕ) :
    ∑ k ∈ Finset.range (n + 1),
        (jacobsthalLucasNumber k : ℚ) * (((n - k : ℕ) : ℚ) / 2 ^ (n - k)) =
      2 / 9 * (jacobsthalLucasNumber (n + 1) : ℚ) - 2 / (9 * 2 ^ n)

Sources

• Michael R. Bacon and Charles K. Cook, Some Properties of Oresme Numbers and Convolutions with Various Second Order Sequences, The Fibonacci Quarterly 62 (2024), no. 3, Article cookbacon061124, Proposition 6.4.

Uses 1

Statement usesJacobsthal–Lucas numbers

TheoremPowers of two times Jacobsthal–Lucas numbers modulo 9#●ready to prove

Let \(j_m\) denote the Jacobsthal–Lucas numbers. For every natural number \(n\), \(2^n j_{n+1} \equiv 1 \pmod{9}\).

public theorem_wanted two_pow_mul_jacobsthalLucasNumber_succ_modEq_nine (n : ℕ) :
    2 ^ n * jacobsthalLucasNumber (n + 1) ≡ 1 [MOD 9]

Sources

• Michael R. Bacon and Charles K. Cook, Some Properties of Oresme Numbers and Convolutions with Various Second Order Sequences, The Fibonacci Quarterly 62 (2024), no. 3, Article cookbacon061124, Corollary 6.5.

Uses 1

Statement usesJacobsthal–Lucas numbers

13 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.