The square root of the factorial beats every geometric progression

The asymptotic input to Deligne §1.20: for any real constants C and c there is an n with C * c ^ n < Real.sqrt n.factorial.

The route is elementary. The integral bound three_pow_mul_factorial_ge (n ^ n ≤ 3 ^ n * n !, from RS/Common/FactorialBound.lean) gives (n / 3) ^ n ≤ n ! over ℝ, so at an even index n = 2 * m the square root of the factorial is at least (2 * m / 3) ^ m. Replacing C and c by max |C| 1 and max |c| 1 reduces every sign case to constants at least 1, and it then suffices to pick m beyond both 3 * b ^ 2 (so the base 2 * m / 3 dominates 2 * b ^ 2) and a natural number exceeding the constant (so the spare factor 2 ^ m swallows it).

theorem RS.div_three_pow_le_factorial (n : ℕ) : (↑n / 3) ^ n ≤ ↑n.factorial

Real form of three_pow_mul_factorial_ge: (n / 3) ^ n ≤ n ! over ℝ.

theorem RS.pow_le_sqrt_factorial_two_mul (m : ℕ) : (↑(2 * m) / 3) ^ m ≤ √↑(2 * m).factorial

At an even index the square root of the factorial dominates (2 * m / 3) ^ m.

theorem RS.exists_lt_sqrt_factorial (C c : ℝ) : ∃ (n : ℕ), C * c ^ n < √↑n.factorial

The square root of the factorial beats every geometric progression: for any real constants C and c there is an n with C * c ^ n < Real.sqrt n.factorial. This is the asymptotic input to Deligne §1.20.