English
If a > 1, then there exists a natural number m such that (m+1) < a^m, illustrating that exponential growth eventually dominates linear growth.
Русский
Пусть a > 1; существует m ∈ ℕ such that (m+1) < a^m, демонстрируя, что экспоненциальный рост в конце концов превосходит линейный.
LaTeX
$$$$\forall a>1, \exists m \in \mathbb{N}, (m+1) < a^m.$$$$
Lean4
/-- Exponentiation is eventually larger than linear growth. -/
theorem exists_natCast_add_one_lt_pow_of_one_lt (ha : 1 < a) : ∃ m : ℕ, (m + 1 : ℝ) < a ^ m :=
by
obtain ⟨k, posk, hk⟩ : ∃ k : ℕ, 0 < k ∧ 1 / k + 1 < a :=
by
contrapose! ha
refine le_of_forall_lt_rat_imp_le ?_
intro q hq
refine (ha q.den (by positivity)).trans ?_
rw [← le_sub_iff_add_le, div_le_iff₀ (by positivity), sub_mul, one_mul]
norm_cast at hq ⊢
rw [← q.num_div_den, one_lt_div (by positivity)] at hq
rw [q.mul_den_eq_num]
norm_cast at hq ⊢
cutsat
use 2 * k ^ 2
calc
((2 * k ^ 2 : ℕ) + 1 : ℝ) ≤ 2 ^ (2 * k) := mod_cast Nat.two_mul_sq_add_one_le_two_pow_two_mul _
_ = (1 / k * k + 1 : ℝ) ^ (2 * k) := by simp [posk.ne']; norm_num
_ ≤ ((1 / k + 1) ^ k : ℝ) ^ (2 * k) := by gcongr; exact mul_add_one_le_add_one_pow (by simp) _
_ = (1 / k + 1 : ℝ) ^ (2 * k ^ 2) := by rw [← pow_mul, mul_left_comm, sq]
_ < a ^ (2 * k ^ 2) := by gcongr
