Aigner's ratio inequality for Motzkin numbers

TheoremAigner's ratio inequality for Motzkin numbers, explicit sum form#✓fully proved

For \(r \ge 0\) let \(M_r = \sum_{k=0}^{\lfloor r/2 \rfloor} \frac{1}{k+1}\binom{2k}{k}\binom{r}{2k}\), where each factor \(\frac{1}{k+1}\binom{2k}{k}\) is the \(k\)-th Catalan number, an integer. Then for every \(n \ge 1\), in the rational numbers,

\[ \frac{M_n - M_{n-1}}{M_{n+1} - M_n} \le \frac{M_n}{M_{n+1}}. \]

theorem aigner_motzkin_ratio_inequality (n : ℕ) (hn : 1 ≤ n) :
    let M : ℕ → ℕ := fun r =>
      ∑ k ∈ Finset.range (r / 2 + 1),
        (Nat.choose (2 * k) k / (k + 1)) * Nat.choose r (2 * k)
    (((M n : ℚ) - (M (n - 1) : ℚ)) /
        ((M (n + 1) : ℚ) - (M n : ℚ))) ≤
      (M n : ℚ) / (M (n + 1) : ℚ)

Sources

• Takashi Agoh and Horst Alzer, "Mean Value Inequalities for Motzkin Numbers", Journal of Integer Sequences 24 (2021), Article 21.6.8: Motzkin-number definition, lines 89--107; Aigner ratio inequality, lines 373--386, equation (11). The same inequality for the canonical MetaMathlibExt.motzkinNumber is motzkinNumber_ratio_inequality.
• https://cs.uwaterloo.ca/journals/JIS/VOL24/Alzer/alzer8.tex.

Used by 1

Used byAigner's ratio inequality for Motzkin numbers

TheoremAigner's ratio inequality for Motzkin numbers#✓fully proved

Let \(M_n\) denote the \(n\)-th Motzkin number. For every \(n \ge 1\),

\[ \frac{M_n - M_{n-1}}{M_{n+1} - M_n} \le \frac{M_n}{M_{n+1}}. \]

theorem motzkinNumber_ratio_inequality (n : ℕ) (hn : 1 ≤ n) :
    ((motzkinNumber n : ℚ) - motzkinNumber (n - 1)) /
        ((motzkinNumber (n + 1) : ℚ) - motzkinNumber n) ≤
      (motzkinNumber n : ℚ) / motzkinNumber (n + 1)

Sources

• Takashi Agoh and Horst Alzer, Mean Value Inequalities for Motzkin Numbers, Journal of Integer Sequences 24 (2021), Article 21.6.8, equation (11).

Uses 3

Statement usesMotzkin numbers as a Catalan-weighted binomial sum

Proof usesAigner's ratio inequality for Motzkin numbers, explicit sum form · Truncated Catalan-weighted sum for Motzkin numbers

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.