Leonardo numbers

DefinitionGeneralized Leonardo numbers#✓fully proved

For an integer \(k\), the generalized Leonardo numbers \(L_{k,0}, L_{k,1}, L_{k,2}, \ldots\) are the integers defined by \(L_{k,0} = L_{k,1} = 1\) and \(L_{k,n+2} = L_{k,n+1} + L_{k,n} + k\) for all \(n \ge 0\).

The paper takes \(k\) positive; here \(k\) may be any integer.

public def genLeonardo (k : ℤ) : ℕ → ℤ
  | 0 => 1
  | 1 => 1
  | n + 2 => genLeonardo k (n + 1) + genLeonardo k n + k
Sources
  • Kuhapatanakul, Note on the Generalized Leonardo Numbers, Fibonacci Quarterly 62.3 (2024), introduction.
Used by 26
Used byInfinitely many Leonardo numbers are not sums of two prime powers · Hyper-Leonardo numbers · First hyper-Leonardo numbers of order one · Consecutive hyper-Leonardo numbers of order one · Hyper-Leonardo numbers of order zero · Generating function of the Leonardo numbers · Leonardo numbers are log-balanced at index three · Log-convexity and log-concavity of the Leonardo numbers · Alternating binomial identities for generalized Leonardo numbers · Binomial identities with steps three and four for generalized Leonardo numbers · Binomial convolution identities for generalized Leonardo numbers · Even-order binomial identities for generalized Leonardo numbers · Dual generalized Leonardo numbers · The dual generalized Leonardo number of index one · Cross-product identity for generalized Leonardo numbers · Generalized Leonardo numbers as Leonardo \(p\)-numbers with \(p = 1\) · Product of a generalized Leonardo number and its dual · Log-concavity of partial sums of generalized Leonardo numbers · Log-convexity of the self-powers of generalized Leonardo numbers · Log-balancedness of the n-th roots of generalized Leonardo numbers · Log-convexity of the n-th roots of generalized Leonardo numbers · Shift identity for generalized Leonardo numbers · Square-difference identity for generalized Leonardo numbers · Sum-and-difference square identities for generalized Leonardo numbers · Generalized Leonardo number of index two · Log-balancedness of the reciprocals of generalized Leonardo numbers

TheoremGeneralized Leonardo number of index two#✓fully proved

For every integer \(k\), the generalized Leonardo number \(L_{k,2}\) equals \(2 + k\).

public theorem genLeonardo_two (k : ℤ) : genLeonardo k 2 = 2 + k
Sources
  • Kuhapatanakul, Note on the Generalized Leonardo Numbers, Fibonacci Quarterly (2024).
Uses 1 · Used by 1
Statement usesGeneralized Leonardo numbers
Used byThe dual generalized Leonardo number of index one

TheoremGeneralized Leonardo numbers as Leonardo \(p\)-numbers with \(p = 1\)#●ready to prove

For all natural numbers \(k\) and \(n\), the generalized Leonardo number \(L_{k,n}\) equals the generalized Leonardo \(p\)-number \(\mathcal{L}_{1,k}(n)\); both sequences start with \(1, 1\) and satisfy the recurrence \(a_{n+2} = a_{n+1} + a_n + k\).

public theorem_wanted genLeonardo_eq_leonardoPK_one (k n : ℕ) :
    genLeonardo (k : ℤ) n
      = MathlibExt.NumberTheory.LeonardoPWanted.leonardoPK 1 k n
Sources
  • Kuhapatanakul, Note on the Generalized Leonardo Numbers, Fibonacci Quarterly 62.3 (2024), introduction; Kusrini, Putra, and Kuhapatanakul, On Generalized Leonardo p-Numbers, Journal of Integer Sequences 27 (2024), Article 24.4.6.
Uses 2
Statement usesGeneralized Leonardo \(p\)-numbers · Generalized Leonardo numbers

DefinitionDual generalized Leonardo numbers#✓fully proved

For an integer \(k\), let \(L_{k,n}\) denote the generalized Leonardo numbers. The dual generalized Leonardo numbers \(M_{k,n}\), for natural numbers \(n\), are defined by \(M_{k,0} = 1 - k\) and \(M_{k,n+1} = L_{k,n} + L_{k,n+2}\), so that \(M_{k,n} = L_{k,n-1} + L_{k,n+1}\) for \(n \ge 1\).

This agrees with the paper's Definition 2.1, which sets \(M_{k,0} = 1 - k\), \(M_{k,1} = k + 3\), and \(M_{k,n+1} = M_{k,n} + M_{k,n-1} + 2k\) for \(n \ge 1\).

public def genLeonardoCompanion (k : ℤ) : ℕ → ℤ
  | 0 => 1 - k
  | n + 1 => genLeonardo k n + genLeonardo k (n + 2)
Sources
  • Kuhapatanakul, Note on the Generalized Leonardo Numbers, Fibonacci Quarterly 62.3 (2024), Definition 2.1 and identity (2.1).
Uses 1 · Used by 8
Statement usesGeneralized Leonardo numbers
Used byAlternating binomial identities for generalized Leonardo numbers · Binomial identities with steps three and four for generalized Leonardo numbers · Binomial convolution identities for generalized Leonardo numbers · Even-order binomial identities for generalized Leonardo numbers · The dual generalized Leonardo number of index one · Cross-product identity for generalized Leonardo numbers · Product of a generalized Leonardo number and its dual · Square-difference identity for generalized Leonardo numbers

TheoremThe dual generalized Leonardo number of index one#✓fully proved

For every integer \(k\), the dual generalized Leonardo number \(M_{k,1}\) equals \(3 + k\).

public theorem genLeonardoCompanion_one (k : ℤ) :
    genLeonardoCompanion k 1 = 3 + k
Sources
  • Kuhapatanakul, Note on the Generalized Leonardo Numbers, Fibonacci Quarterly (2024).
Uses 3
Statement usesDual generalized Leonardo numbers
Proof usesGeneralized Leonardo numbers · Generalized Leonardo number of index two

TheoremProduct of a generalized Leonardo number and its dual#●ready to prove

Let \(k\) be an integer, and let \(L_{k,n}\) and \(M_{k,n}\) denote the generalized Leonardo numbers and the dual generalized Leonardo numbers. For every natural number \(n\),

\[L_{k,n} M_{k,n} = (k+1) L_{k,2n+1} - k L_{k,n+3} + k\,(2k+1).\]
public theorem_wanted genLeonardo_mul_companion (k : ℤ) (n : ℕ) :
    genLeonardo k n * genLeonardoCompanion k n
      = (k + 1) * genLeonardo k (2 * n + 1) - k * genLeonardo k (n + 3)
        + k * (2 * k + 1)
Sources
  • Kuhapatanakul, Note on the Generalized Leonardo Numbers, Fibonacci Quarterly (2024), Theorem 2.2.
Uses 2
Statement usesGeneralized Leonardo numbers · Dual generalized Leonardo numbers

TheoremCross-product identity for generalized Leonardo numbers#●ready to prove

Let \(k\) be an integer, and let \(L_{k,n}\) and \(M_{k,n}\) denote the generalized Leonardo numbers and the dual generalized Leonardo numbers. For every natural number \(n \ge 1\),

\[L_{k,n} M_{k,n+1} - L_{k,n+1} M_{k,n-1} = (k+1) L_{k,2n} - k L_{k,n} + k.\]
public theorem_wanted genLeonardo_cross (k : ℤ) (n : ℕ) (hn : 1 ≤ n) :
    genLeonardo k n * genLeonardoCompanion k (n + 1)
        - genLeonardo k (n + 1) * genLeonardoCompanion k (n - 1)
      = (k + 1) * genLeonardo k (2 * n) - k * genLeonardo k n + k
Sources
  • Kuhapatanakul, Note on the Generalized Leonardo Numbers, Fibonacci Quarterly (2024), Theorem 2.3.
Uses 2
Statement usesGeneralized Leonardo numbers · Dual generalized Leonardo numbers

TheoremSquare-difference identity for generalized Leonardo numbers#●ready to prove

For every integer \(k\) and every natural number \(n \ge 1\), the generalized Leonardo numbers \(L_{k,n}\) and the dual generalized Leonardo numbers \(M_{k,n}\) satisfy

\[M_{k,n}^2 - L_{k,n}^2 = 4 L_{k,n-1} L_{k,n+1} + 2k L_{k,n} + k^2.\]
public theorem_wanted genLeonardo_sq_sub_sq (k : ℤ) (n : ℕ) (hn : 1 ≤ n) :
    genLeonardoCompanion k n ^ 2 - genLeonardo k n ^ 2
      = 4 * genLeonardo k (n - 1) * genLeonardo k (n + 1)
        + 2 * k * genLeonardo k n + k ^ 2
Sources
  • Kuhapatanakul, Note on the Generalized Leonardo Numbers, Fibonacci Quarterly (2024), Theorem 2.4.
Uses 2
Statement usesGeneralized Leonardo numbers · Dual generalized Leonardo numbers

TheoremShift identity for generalized Leonardo numbers#●ready to prove

Let \(k\) be an integer and let \(L_{k,n}\) denote the generalized Leonardo numbers. For all natural numbers \(m\), \(n\), \(t\) with \(1 \le t \le n\) and \(n + 1 \le m + t\),

\[L_{k,m} L_{k,n} - L_{k,m+t} L_{k,n-t} = (-1)^{n-t+1} (L_{k,m+t-n-1} + k)(L_{k,t-1} + k) - k\,(L_{k,m} + L_{k,n} - L_{k,m+t} - L_{k,n-t}).\]

The paper also allows \(t = 0\), reading \(L_{k,-1}\) by extending the sequence to negative indices.

public theorem_wanted genLeonardo_shift (k : ℤ) (m n t : ℕ)
    (ht : 1 ≤ t) (htn : t ≤ n) (hmt : n + 1 ≤ m + t) :
    genLeonardo k m * genLeonardo k n
        - genLeonardo k (m + t) * genLeonardo k (n - t)
      = (-1 : ℤ) ^ (n - t + 1)
          * (genLeonardo k (m + t - n - 1) + k) * (genLeonardo k (t - 1) + k)
        - k * (genLeonardo k m + genLeonardo k n
          - genLeonardo k (m + t) - genLeonardo k (n - t))
Sources
  • Kuhapatanakul, Note on the Generalized Leonardo Numbers, Fibonacci Quarterly (2024), Theorem 2.5.
Uses 1
Statement usesGeneralized Leonardo numbers

TheoremSum-and-difference square identities for generalized Leonardo numbers#●ready to prove

For every integer \(k\) and all natural numbers \(m\), \(n\) with \(1 \le n < m\), the generalized Leonardo numbers \(L_{k,n}\) satisfy

\[L_{k,m+n}^2 - L_{k,m-n}^2 = (L_{k,2m+1} + k)(L_{k,2n-1} + k) - 2k (L_{k,m+n} - L_{k,m-n})\]

and

\[L_{k,m+n}^2 + L_{k,m-n-1}^2 = (L_{k,2m} + k)(L_{k,2n} + k) - 2k (L_{k,m+n} + L_{k,m-n-1}) - 2k^2.\]

In the second identity the last term inside the parentheses is \(L_{k,m-n-1}\). The paper as printed shows \(L_{k,m-n}\) there, which is false: at \(k = 1\), \(m = 3\), \(n = 1\) the printed identity reads \(82 = 78\). The reading used here agrees with the paper's outline derivation.

public theorem_wanted genLeonardo_sq_sum_diff (k : ℤ) (m n : ℕ)
    (hn : 1 ≤ n) (hmn : n < m) :
    (genLeonardo k (m + n) ^ 2 - genLeonardo k (m - n) ^ 2
      = (genLeonardo k (2 * m + 1) + k) * (genLeonardo k (2 * n - 1) + k)
        - 2 * k * (genLeonardo k (m + n) - genLeonardo k (m - n))) ∧
    (genLeonardo k (m + n) ^ 2 + genLeonardo k (m - n - 1) ^ 2
      = (genLeonardo k (2 * m) + k) * (genLeonardo k (2 * n) + k)
        - 2 * k * (genLeonardo k (m + n) + genLeonardo k (m - n - 1))
        - 2 * k ^ 2)
Sources
  • Kuhapatanakul, Note on the Generalized Leonardo Numbers, Fibonacci Quarterly (2024), Theorem 2.6.
Uses 1
Statement usesGeneralized Leonardo numbers

TheoremBinomial convolution identities for generalized Leonardo numbers#●ready to prove

Let \(k\) be an integer, and let \(L_{k,n}\) and \(M_{k,n}\) denote the generalized Leonardo numbers and the dual generalized Leonardo numbers. For all natural numbers \(n\) and \(r\),

\[\sum_{i=0}^{n} \binom{n}{i} L_{k,i+r} = L_{k,2n+r} - k\,(2^n - 1)\]

and

\[\sum_{i=0}^{n} \binom{n}{i} M_{k,i+r} = M_{k,2n+r} - 2k\,(2^n - 1).\]

Parts (iii) and (iv) of the paper's Theorem 3.1, alternating sums involving the index \(L_{k,n-r-2}\), are false as printed: at \(k = 1\), \(n = 3\), \(r = 1\), with the sequence extended to negative indices by the recurrence, the left side is \(2\) and the printed right side is \(-2\).

public theorem_wanted genLeonardo_binomial_sum (k : ℤ) (n r : ℕ) :
    (∑ i ∈ Finset.range (n + 1), (Nat.choose n i : ℤ) * genLeonardo k (i + r)
      = genLeonardo k (2 * n + r) - k * (2 ^ n - 1)) ∧
    (∑ i ∈ Finset.range (n + 1), (Nat.choose n i : ℤ) * genLeonardoCompanion k (i + r)
      = genLeonardoCompanion k (2 * n + r) - 2 * k * (2 ^ n - 1))
Sources
  • Kuhapatanakul, Note on the Generalized Leonardo Numbers, Fibonacci Quarterly (2024), Theorem 3.1 (i),(ii).
Uses 2
Statement usesGeneralized Leonardo numbers · Dual generalized Leonardo numbers

TheoremEven-order binomial identities for generalized Leonardo numbers#●ready to prove

Let \(k\) be an integer, and let \(L_{k,n}\) and \(M_{k,n}\) denote the generalized Leonardo numbers and the dual generalized Leonardo numbers. For all natural numbers \(m\) and \(r\),

\[\sum_{i=0}^{2m} \binom{2m}{i} L_{k,2i+r} = 5^m L_{k,2m+r} + k\,(5^m - 2^{2m})\]

and

\[\sum_{i=0}^{2m} \binom{2m}{i} M_{k,2i+r} = 5^m M_{k,2m+r} + 2k\,(5^m - 2^{2m}).\]

The paper's Theorem 3.2 also states identities of odd order \(n\); as printed they are false (at \(k = n = 1\), \(r = 0\) the first odd identity reads \(4 = 6\)).

public theorem_wanted genLeonardo_binomial_sum_two_mul (k : ℤ) (m r : ℕ) :
    (∑ i ∈ Finset.range (2 * m + 1),
        (Nat.choose (2 * m) i : ℤ) * genLeonardo k (2 * i + r)
      = 5 ^ m * genLeonardo k (2 * m + r) + k * (5 ^ m - 2 ^ (2 * m))) ∧
    (∑ i ∈ Finset.range (2 * m + 1),
        (Nat.choose (2 * m) i : ℤ) * genLeonardoCompanion k (2 * i + r)
      = 5 ^ m * genLeonardoCompanion k (2 * m + r) + 2 * k * (5 ^ m - 2 ^ (2 * m)))
Sources
  • Kuhapatanakul, Note on the Generalized Leonardo Numbers, Fibonacci Quarterly (2024), Theorem 3.2, even case.
Uses 2
Statement usesGeneralized Leonardo numbers · Dual generalized Leonardo numbers

TheoremAlternating binomial identities for generalized Leonardo numbers#●ready to prove

Let \(k\) be an integer, and let \(L_{k,n}\) and \(M_{k,n}\) denote the generalized Leonardo numbers and the dual generalized Leonardo numbers. For all natural numbers \(n \ge 1\) and \(r\),

\[\sum_{i=0}^{n} \binom{n}{i} (-1)^{n-i} L_{k,2i+r} = L_{k,n+r} + k\]

and

\[\sum_{i=0}^{n} \binom{n}{i} (-1)^{n-i} M_{k,2i+r} = M_{k,n+r} + 2k.\]

The hypothesis \(n \ge 1\) is needed: for \(n = 0\) the two sums equal \(L_{k,r}\) and \(M_{k,r}\).

public theorem_wanted genLeonardo_binomial_alternating (k : ℤ) (n r : ℕ)
    (hn : 1 ≤ n) :
    (∑ i ∈ Finset.range (n + 1),
        (Nat.choose n i : ℤ) * (-1) ^ (n - i) * genLeonardo k (2 * i + r)
      = genLeonardo k (n + r) + k) ∧
    (∑ i ∈ Finset.range (n + 1),
        (Nat.choose n i : ℤ) * (-1) ^ (n - i) * genLeonardoCompanion k (2 * i + r)
      = genLeonardoCompanion k (n + r) + 2 * k)
Sources
  • Kuhapatanakul, Note on the Generalized Leonardo Numbers, Fibonacci Quarterly (2024), Theorem 3.3.
Uses 2
Statement usesGeneralized Leonardo numbers · Dual generalized Leonardo numbers

TheoremBinomial identities with steps three and four for generalized Leonardo numbers#●ready to prove

Let \(k\) be an integer, and let \(L_{k,n}\) and \(M_{k,n}\) denote the generalized Leonardo numbers and the dual generalized Leonardo numbers. For all natural numbers \(n\) and \(r\),

\[\sum_{i=0}^{n} \binom{n}{i} L_{k,3i+r} = 2^n L_{k,2n+r},\]
\[\sum_{i=0}^{n} \binom{n}{i} M_{k,3i+r} = 2^n M_{k,2n+r},\]
\[\sum_{i=0}^{n} \binom{n}{i} L_{k,4i+r} = 3^n L_{k,2n+r} + k\,(3^n - 2^n),\]

and

\[\sum_{i=0}^{n} \binom{n}{i} M_{k,4i+r} = 3^n M_{k,2n+r} + 2k\,(3^n - 2^n).\]

Part (iv) of the paper's Theorem 3.4 prints the last term of the fourth identity as \(k\,(3^n - 2^n)\), which is false at \(k = n = 1\), \(r = 0\); the coefficient \(2k\) is the correct one, as in parts (ii) of Theorems 3.1–3.3.

public theorem_wanted genLeonardo_binomial_steps (k : ℤ) (n r : ℕ) :
    (∑ i ∈ Finset.range (n + 1), (Nat.choose n i : ℤ) * genLeonardo k (3 * i + r)
      = 2 ^ n * genLeonardo k (2 * n + r)) ∧
    (∑ i ∈ Finset.range (n + 1), (Nat.choose n i : ℤ) * genLeonardoCompanion k (3 * i + r)
      = 2 ^ n * genLeonardoCompanion k (2 * n + r)) ∧
    (∑ i ∈ Finset.range (n + 1), (Nat.choose n i : ℤ) * genLeonardo k (4 * i + r)
      = 3 ^ n * genLeonardo k (2 * n + r) + k * (3 ^ n - 2 ^ n)) ∧
    (∑ i ∈ Finset.range (n + 1), (Nat.choose n i : ℤ) * genLeonardoCompanion k (4 * i + r)
      = 3 ^ n * genLeonardoCompanion k (2 * n + r) + 2 * k * (3 ^ n - 2 ^ n))
Sources
  • Kuhapatanakul, Note on the Generalized Leonardo Numbers, Fibonacci Quarterly (2024), Theorem 3.4.
Uses 2
Statement usesGeneralized Leonardo numbers · Dual generalized Leonardo numbers

TheoremLog-concavity propagates along a linear recurrence#●ready to prove

Let \(k \ge 2\) be an integer, let \(c_1, \dots, c_k\) be real numbers with \(c_j \ge 0\) for \(2 \le j \le k\), and let \((z_n)_{n \ge 0}\) be a sequence of positive real numbers with

\[z_n = c_1 z_{n-1} - \sum_{j=2}^{k} c_j z_{n-j} \quad (n \ge k).\]

If \(z_{i-1} z_{i+1} \le z_i^2\) for \(1 \le i < k\), then \(z_{n-1} z_{n+1} \le z_n^2\) for every \(n \ge 1\); that is, the whole sequence is log-concave.

The paper assumes that the block \(z_0, \dots, z_{k+1}\) is log-concave, which adds the inequality for \(i = k\), and that \(c_1 > 0\). Both follow from the other hypotheses: the recurrence at \(n = k + 1\) propagates the inequality for \(i = k\) from those for \(i < k\), and the recurrence at \(n = k\) forces \(c_1 > 0\).

public theorem_wanted logConcave_of_linearRecurrence_of_initial_logConcave
    (k : ℕ) (hk : 2 ≤ k) (c : ℕ → ℝ) (hc : ∀ j, 2 ≤ j → j ≤ k → 0 ≤ c j)
    (z : ℕ → ℝ) (hpos : ∀ n, 0 < z n)
    (hrec : ∀ n, k ≤ n →
      z n = c 1 * z (n - 1) - ∑ j ∈ Finset.Icc 2 k, c j * z (n - j))
    (hinit : ∀ i, 1 ≤ i → i < k → z (i - 1) * z (i + 1) ≤ z i ^ 2) :
    ∀ n, 1 ≤ n → z (n - 1) * z (n + 1) ≤ z n ^ 2
Sources
  • Feng-Zhen Zhao, The Log-Behavior of Some Sequences Related to the Generalized Leonardo Numbers, INTEGERS 24 (2024), Article A82, Lemma 1 (quoted from the paper's reference [17]).

TheoremLog-convexity propagates along a linear recurrence#●ready to prove

Let \(k \ge 2\) be an integer, let \(c_1, \dots, c_k\) be real numbers with \(c_j \ge 0\) for \(2 \le j \le k\), and let \((z_n)_{n \ge 0}\) be a sequence of positive real numbers with

\[z_n = c_1 z_{n-1} - \sum_{j=2}^{k} c_j z_{n-j} \quad (n \ge k).\]

If \(z_i^2 \le z_{i-1} z_{i+1}\) for \(1 \le i < k\), then \(z_n^2 \le z_{n-1} z_{n+1}\) for every \(n \ge 1\); that is, the whole sequence is log-convex.

The paper assumes that the block \(z_0, \dots, z_{k+1}\) is log-convex, which adds the inequality for \(i = k\), and that \(c_1 > 0\). Both follow from the other hypotheses: the recurrence propagates the inequality for \(i = k\), and the recurrence at \(n = k\) forces \(c_1 > 0\).

public theorem_wanted logConvex_of_linearRecurrence_of_initial_logConvex
    (k : ℕ) (hk : 2 ≤ k) (c : ℕ → ℝ) (hc : ∀ j, 2 ≤ j → j ≤ k → 0 ≤ c j)
    (z : ℕ → ℝ) (hpos : ∀ n, 0 < z n)
    (hrec : ∀ n, k ≤ n →
      z n = c 1 * z (n - 1) - ∑ j ∈ Finset.Icc 2 k, c j * z (n - j))
    (hinit : ∀ i, 1 ≤ i → i < k → z i ^ 2 ≤ z (i - 1) * z (i + 1)) :
    ∀ n, 1 ≤ n → z n ^ 2 ≤ z (n - 1) * z (n + 1)
Sources
  • Feng-Zhen Zhao, The Log-Behavior of Some Sequences Related to the Generalized Leonardo Numbers, INTEGERS 24 (2024), Article A82, Lemma 1, log-convex reading (quoted from the paper's reference [17]).

TheoremLog-balancedness of reciprocals along a three-term recurrence#●ready to prove

Let \(c_1\) and \(c_2\) be real numbers with \(c_2 \ge 0\), and let \((z_n)_{n \ge 0}\) be a sequence of positive real numbers with \(z_{n+1} = c_1 z_n - c_2 z_{n-2}\) for every \(n \ge 2\). Write \(w_n = 1/z_n\) and \(x_n = z_{n+1}/z_n\), and let \(n_0 \ge 0\) be an integer. Suppose that for \(n = n_0 + 1\) and \(n = n_0 + 2\)

\[w_n^2 \le w_{n-1} w_{n+1} \quad \text{and} \quad \frac{w_{n-1}}{(n-1)!} \cdot \frac{w_{n+1}}{(n+1)!} \le \left(\frac{w_n}{n!}\right)^2,\]

and that \(c_1 x_n x_{n+1} \ge 3 c_2\) for every \(n \ge n_0\). Then both inequalities hold for every \(n \ge n_0 + 1\); that is, the sequence \((1/z_n)_{n \ge n_0}\) is log-balanced (Došlić).

The paper also assumes \(c_1 > 0\); this follows from positivity, the recurrence and \(c_2 \ge 0\).

public theorem_wanted inv_logBalanced_of_recurrence_of_initial (c₁ c₂ : ℝ) (hc₂ : 0 ≤ c₂)
    (z : ℕ → ℝ) (hpos : ∀ n, 0 < z n)
    (hrec : ∀ n, 2 ≤ n → z (n + 1) = c₁ * z n - c₂ * z (n - 2)) (n₀ : ℕ)
    (hinit : ∀ n, n₀ + 1 ≤ n → n ≤ n₀ + 2 →
      (1 / z n) ^ 2 ≤ (1 / z (n - 1)) * (1 / z (n + 1)) ∧
        (1 / z (n - 1) / (n - 1).factorial) * (1 / z (n + 1) / (n + 1).factorial) ≤
          (1 / z n / n.factorial) ^ 2)
    (hx : ∀ n, n₀ ≤ n → 3 * c₂ ≤ c₁ * (z (n + 1) / z n) * (z (n + 2) / z (n + 1))) :
    ∀ n, n₀ + 1 ≤ n →
      (1 / z n) ^ 2 ≤ (1 / z (n - 1)) * (1 / z (n + 1)) ∧
        (1 / z (n - 1) / (n - 1).factorial) * (1 / z (n + 1) / (n + 1).factorial) ≤
          (1 / z n / n.factorial) ^ 2
Sources
  • Feng-Zhen Zhao, The Log-Behavior of Some Sequences Related to the Generalized Leonardo Numbers, INTEGERS 24 (2024), Article A82, Lemma 2.

TheoremLog-balancedness of the reciprocals of generalized Leonardo numbers#●ready to prove

Let \(k \ge 1\) be an integer and let \(L_{k,n}\) be the generalized Leonardo numbers. Then the sequence \((1/L_{k,n})_{n \ge 3}\) is log-balanced (Došlić): for every integer \(n \ge 4\),

\[\left(\frac{1}{L_{k,n}}\right)^2 \le \frac{1}{L_{k,n-1}} \cdot \frac{1}{L_{k,n+1}}\]

and

\[\frac{1}{L_{k,n-1} \, (n-1)!} \cdot \frac{1}{L_{k,n+1} \, (n+1)!} \le \left(\frac{1}{L_{k,n} \, n!}\right)^2.\]
public theorem_wanted inv_genLeonardo_logBalanced (k : ℕ) (hk : 1 ≤ k) (n : ℕ) (hn : 4 ≤ n) :
    (1 / (genLeonardo k n : ℝ)) ^ 2 ≤
        (1 / (genLeonardo k (n - 1) : ℝ)) * (1 / (genLeonardo k (n + 1) : ℝ)) ∧
      (1 / (genLeonardo k (n - 1) : ℝ) / (n - 1).factorial) *
          (1 / (genLeonardo k (n + 1) : ℝ) / (n + 1).factorial) ≤
        (1 / (genLeonardo k n : ℝ) / n.factorial) ^ 2
Sources
  • Feng-Zhen Zhao, The Log-Behavior of Some Sequences Related to the Generalized Leonardo Numbers, INTEGERS 24 (2024), Article A82, Theorem 1.
Uses 1
Statement usesGeneralized Leonardo numbers

TheoremLog-convexity of the n-th roots of generalized Leonardo numbers#●ready to prove

Let \(k \ge 1\) be an integer and let \(L_{k,n}\) be the generalized Leonardo numbers. Then the sequence \((L_{k,n}^{1/n})_{n \ge 9}\) is log-convex: \((L_{k,n}^{1/n})^2 \le L_{k,n-1}^{1/(n-1)} L_{k,n+1}^{1/(n+1)}\) for every integer \(n \ge 10\).

public theorem_wanted genLeonardo_rpow_inv_logConvex (k : ℕ) (hk : 1 ≤ k) (n : ℕ)
    (hn : 10 ≤ n) :
    ((genLeonardo k n : ℝ) ^ ((1 : ℝ) / n)) ^ 2 ≤
      (genLeonardo k (n - 1) : ℝ) ^ ((1 : ℝ) / (n - 1 : ℕ)) *
        (genLeonardo k (n + 1) : ℝ) ^ ((1 : ℝ) / (n + 1 : ℕ))
Sources
  • Feng-Zhen Zhao, The Log-Behavior of Some Sequences Related to the Generalized Leonardo Numbers, INTEGERS 24 (2024), Article A82, Theorem 3.
Uses 1
Statement usesGeneralized Leonardo numbers

TheoremLog-concavity of partial sums of generalized Leonardo numbers#●ready to prove

Let \(k \ge 1\) be an integer, let \(L_{k,n}\) be the generalized Leonardo numbers, and let \(R_n = \sum_{i=0}^{n} L_{k,i}\). Then \(R_{n-1} R_{n+1} \le R_n^2\) for every integer \(n \ge 2\).

The inequality fails at \(n = 1\): there \(R_0 = 1\), \(R_1 = 2\) and \(R_2 = k + 4\), so \(R_1^2 - R_0 R_2 = -k < 0\). The paper states it for every \(n \ge 1\), although its identity \(R_n^2 - R_{n-1} R_{n+1} = (k+1)^2 (F_n + (-1)^n) + k(k+1)(n F_n - 2 F_{n+1}) + k^2\), with \(F_n\) the Fibonacci numbers, gives the same value \(-k\) at \(n = 1\).

public theorem_wanted genLeonardo_partialSum_logConcave (k : ℕ) (hk : 1 ≤ k) (n : ℕ)
    (hn : 2 ≤ n) :
    (∑ i ∈ Finset.range n, genLeonardo k i) * (∑ i ∈ Finset.range (n + 2), genLeonardo k i) ≤
      (∑ i ∈ Finset.range (n + 1), genLeonardo k i) ^ 2
Sources
  • Feng-Zhen Zhao, The Log-Behavior of Some Sequences Related to the Generalized Leonardo Numbers, INTEGERS 24 (2024), Article A82, Theorem 2.
Uses 1
Statement usesGeneralized Leonardo numbers

TheoremLog-balancedness of the n-th roots of generalized Leonardo numbers#●ready to prove

Let \(k \ge 1\) be an integer, let \(L_{k,n}\) be the generalized Leonardo numbers, and let \(n_k\) be an integer with \(n_k \ge 9\) and \(n_k \ge (1 + \sqrt{64k - 7})/4\). Then for every integer \(n \ge n_k + 1\),

\[\left(L_{k,n}^{1/n}\right)^2 \le L_{k,n-1}^{1/(n-1)} L_{k,n+1}^{1/(n+1)}\]

and

\[\frac{L_{k,n-1}^{1/(n-1)}}{(n-1)!} \cdot \frac{L_{k,n+1}^{1/(n+1)}}{(n+1)!} \le \left(\frac{L_{k,n}^{1/n}}{n!}\right)^2;\]

that is, the sequence \((L_{k,n}^{1/n})_{n \ge n_k}\) is log-balanced (Došlić): it is log-convex and its quotient by \(n!\) is log-concave.

The paper asserts only that some \(n_k \ge \max\{9, (1 + \sqrt{64k - 7})/4\}\) with this property exists; the statement above gives the threshold its proof establishes (log-concavity of \(L_{k,n}^{1/n}/n!\) once \(n \ge (1 + \sqrt{64k - 7})/4\), log-convexity of \(L_{k,n}^{1/n}\) from \(n = 9\) on).

public theorem_wanted genLeonardo_rpow_inv_logBalanced (k : ℕ) (hk : 1 ≤ k) (nk : ℕ)
    (h9 : 9 ≤ nk) (hsqrt : (1 + Real.sqrt (64 * k - 7)) / 4 ≤ nk) :
    ∀ n : ℕ, nk + 1 ≤ n →
      ((genLeonardo k n : ℝ) ^ ((1 : ℝ) / n)) ^ 2 ≤
          (genLeonardo k (n - 1) : ℝ) ^ ((1 : ℝ) / (n - 1 : ℕ)) *
            (genLeonardo k (n + 1) : ℝ) ^ ((1 : ℝ) / (n + 1 : ℕ)) ∧
        (genLeonardo k (n - 1) : ℝ) ^ ((1 : ℝ) / (n - 1 : ℕ)) / (n - 1).factorial *
            ((genLeonardo k (n + 1) : ℝ) ^ ((1 : ℝ) / (n + 1 : ℕ)) / (n + 1).factorial) ≤
          ((genLeonardo k n : ℝ) ^ ((1 : ℝ) / n) / n.factorial) ^ 2
Sources
  • Feng-Zhen Zhao, The Log-Behavior of Some Sequences Related to the Generalized Leonardo Numbers, INTEGERS 24 (2024), Article A82, Theorem 4.
Uses 1
Statement usesGeneralized Leonardo numbers

TheoremLog-convexity of the self-powers of generalized Leonardo numbers#●ready to prove

Let \(k \ge 1\) be an integer and let \(L_{k,n}\) be the generalized Leonardo numbers. Then the sequence \((L_{k,n}^n)_{n \ge 3}\) is log-convex: \(L_{k,n}^{2n} \le L_{k,n-1}^{n-1} L_{k,n+1}^{n+1}\) for every integer \(n \ge 4\).

public theorem_wanted genLeonardo_pow_self_logConvex (k : ℕ) (hk : 1 ≤ k) (n : ℕ)
    (hn : 4 ≤ n) :
    genLeonardo k n ^ (2 * n) ≤ genLeonardo k (n - 1) ^ (n - 1) * genLeonardo k (n + 1) ^ (n + 1)
Sources
  • Feng-Zhen Zhao, The Log-Behavior of Some Sequences Related to the Generalized Leonardo Numbers, INTEGERS 24 (2024), Article A82, Theorem 5.
Uses 1
Statement usesGeneralized Leonardo numbers
4 fully proved18 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.