Central binomial bounds for coefficient estimates

The largest binomial coefficient in row k, multiplied by √(k + 1), is at most 2 ^ k. Together with the supermultiplicativity of the middle coefficients, this combines the coefficient-to-Mahler and Landau bounds without an extra degree factor.

References

• Xiaorun Wu, Diophantine geometry, week 08: arithmetic heights (2023), Lemma 3.5.
• Lukas Pottmeyer, Diophantine Approximation (2022), Lemmas 3.2.8 and 3.2.9.

theorem Nat.centralBinom_mul_sqrt_le_four_pow (n : ℕ) : ↑n.centralBinom * √(2 * ↑n + 1) ≤ 4 ^ n

The central binomial coefficient satisfies the square-root upper bound C(2n,n) √(2n+1) ≤ 4^n.

theorem Nat.choose_middle_mul_sqrt_le_two_pow (k : ℕ) : ↑(k.choose (k / 2)) * √(↑k + 1) ≤ 2 ^ k

The largest binomial coefficient in row k, times √(k+1), is at most 2^k.

theorem Nat.choose_middle_mul_choose_middle_le (a b : ℕ) : a.choose (a / 2) * b.choose (b / 2) ≤ (a + b).choose ((a + b) / 2)

Middle binomial coefficients are supermultiplicative in the row index.

theorem Nat.prod_choose_middle_le_choose_sum_middle {ι : Type u_1} (s : Finset ι) (d : ι → ℕ) : ∏ i ∈ s, (d i).choose (d i / 2) ≤ (∑ i ∈ s, d i).choose ((∑ i ∈ s, d i) / 2)

A finite product of middle binomial coefficients is bounded by the middle coefficient of the sum of their row indices.