eventually_mul_pow_lt_factorial_sub

English

There exists an eventual inequality between an exponential and a shifted factorial, showing c^n < (n-d)! eventually for fixed c,d.

Русский

Существуют такие числа, что c^n < (n-d)! для больших n.

LaTeX

$$$\forall c,d \in \mathbb{N}, \; \forall^{\infty} n, \ c^{n} < (n-d)!$$$

Lean4

theorem eventually_mul_pow_lt_factorial_sub (a c d : ℕ) : ∀ᶠ n in atTop, a * c ^ n < (n - d)! :=
  by
  filter_upwards [Nat.eventually_pow_lt_factorial_sub (a * c) d, Filter.eventually_gt_atTop 0] with n hn hn0
  rw [mul_pow] at hn
  exact (Nat.mul_le_mul_right _ (Nat.le_self_pow hn0.ne' _)).trans_lt hn

Похожие утверждения