`n ^ n ≤ 3 ^ n · n !` #

The crude exponential comparison behind the Schur package's square-dimension growth, proved over ℕ so that the package's arithmetic stays integral.

The route is elementary: expand (n + 1) ^ n binomially, observe that from the second term on each term is at most half the one before it (the identity C(n,k+1)·(k+1) = C(n,k)·(n−k)), and sum a halving sequence to at most twice its first term. That gives (n + 1) ^ n ≤ 3 · n ^ n, and induction turns it into the stated bound.

The constant 3 is deliberate slack: this bound only has to beat some exponential. The sharp comparison n ^ n ≤ e ^ n · n !, which the ⌊2eR⌋ threshold does need, is pow_le_exp_mul_factorial in RS/Classical/SchurTheory/SquareGrowthSharp.lean.

Geometric-sum bound #

If a sequence halves at each step, the partial sum is at most twice the first term.

source

theorem RS.sum_le_two_mul_first (m : ℕ) (f : ℕ → ℕ) :

(∀ (i : ℕ), 2 * f (i + 1) ≤ f i) → ∑ i ∈ Finset.range (m + 1), f i ≤ 2 * f 0

If 2 * f(i+1) ≤ f(i) for all i, then ∑ i in range (m+1), f i ≤ 2 * f 0.

Ratio bound for binomial-expansion terms #

Each successive term in the expansion of (N+1)^N is at most half the previous, starting from the second term. The proof pivots on the identity choose N (k+1) * (k+1) = choose N k * (N - k).

source

theorem RS.binom_term_ratio (N k : ℕ) (hk : 1 ≤ k) (hkN : k + 1 ≤ N) :

2 * (N.choose (k + 1) * N ^ (N - (k + 1))) ≤ N.choose k * N ^ (N - k)

For k ≥ 1 and k + 1 ≤ N, consecutive binomial-expansion terms satisfy 2 * (C(N,k+1) * N^(N-k-1)) ≤ C(N,k) * N^(N-k).

Sub-lemma: `(n+1)^n ≤ 3 * n^n` #

Expand (n+1)^n via the binomial theorem; the m = 0 and m = 1 terms each contribute n^n, and the remaining terms form a geometrically decaying sum bounded by n^n, for a total of at most 3 * n^n.

source

theorem RS.succ_pow_le_three_mul_pow (n : ℕ) :

(n + 1) ^ n ≤ 3 * n ^ n

(n + 1) ^ n ≤ 3 * n ^ n for all natural numbers n.