remainder_lt — Mathlib

English

If m ≥ 2, then remainder m n < 1 / (m^n!)^n for all n ∈ ℕ.

Русский

Если m ≥ 2, тогда remainder m n < 1 / (m^n!)^n для всех n ∈ ℕ.

LaTeX

$$$ \forall n \in \mathbb N,\ \forall m \in \mathbb R,\ 2 \le m \Rightarrow \mathrm{remainder}(m,n) < \frac{1}{(m^{n!})^{n}}$$$

Lean4

/-- An upper estimate on the remainder. This estimate works with `m ∈ ℝ` satisfying `2 ≤ m` and is
weaker than the estimate `LiouvilleNumber.remainder_lt'` above. However, this estimate is
more useful for the proof. -/
theorem remainder_lt (n : ℕ) {m : ℝ} (m2 : 2 ≤ m) : remainder m n < 1 / (m ^ n !) ^ n :=
  (remainder_lt' n <| one_lt_two.trans_le m2).trans_le (aux_calc _ m2)

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