English
In a locally finite ordered ring with a floor semiring structure, for any a, c in the ring and any natural d, the sequence a c^n is eventually strictly smaller than (n − d)!; i.e., factorial growth dominates exponential growth.
Русский
В локально конечном упорядоченном кольце с структурой floor-semirриг, для любых a, c и натурального d, существует N, такое что для всех n ≥ N выполняется a c^n < (n − d)!.
LaTeX
$$$\\forall a,c\\in K,\\; \\forall d\\in\\mathbb{N},\\; \\forall^{\\infty} n\\in\\mathbb{N},\\; a\\, c^n < (n-d)!$$$
Lean4
theorem eventually_mul_pow_lt_factorial_sub (a c : K) (d : ℕ) : ∀ᶠ n in atTop, a * c ^ n < (n - d)! :=
by
filter_upwards [Nat.eventually_mul_pow_lt_factorial_sub ⌈|a|⌉₊ ⌈|c|⌉₊ d] with n h
calc
a * c ^ n
_ ≤ |a * c ^ n| := (le_abs_self _)
_ ≤ ⌈|a|⌉₊ * (⌈|c|⌉₊ : K) ^ n := ?_
_ = ↑(⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n) := ?_
_ < (n - d)! := Nat.cast_lt.mpr h
· rw [abs_mul, abs_pow]
gcongr <;>
try
first
| positivity
| apply Nat.le_ceil
· simp_rw [Nat.cast_mul, Nat.cast_pow]
