English
For n ∈ ℕ and m ∈ ℝ with m > 1, the remainder satisfies remainder m n < (1 − 1/m)^{-1} · (1 / m^{(n+1)!}).
Русский
Для n ∈ ℕ и m ∈ ℝ с m > 1 остаток удовлетворяет remainder m n < (1 − 1/m)^{-1} · (1 / m^{(n+1)!}).
LaTeX
$$$ \forall n \in \mathbb N,\ \forall m \in \mathbb R,\ 1 < m\Rightarrow \mathrm{remainder}(m,n) < \left(1 - \frac{1}{m}\right)^{-1} \cdot \frac{1}{m^{(n+1)!}} $$$
Lean4
/-- An upper estimate on the remainder. This estimate works with `m ∈ ℝ` satisfying `1 < m` and is
stronger than the estimate `LiouvilleNumber.remainder_lt` below. However, the latter estimate is
more useful for the proof. -/
theorem remainder_lt' (n : ℕ) {m : ℝ} (m1 : 1 < m) : remainder m n < (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) :=
-- two useful inequalities
have m0 : 0 < m := zero_lt_one.trans m1
have mi : 1 / m < 1 := (div_lt_one m0).mpr m1
calc
(∑' i, 1 / m ^ (i + (n + 1))!) < ∑' i, 1 / m ^ (i + (n + 1)!) :=
-- 1. the second series dominates the first
Summable.tsum_lt_tsum
(fun b => one_div_pow_le_one_div_pow_of_le m1.le (b.add_factorial_succ_le_factorial_add_succ n))
-- 2. the term with index `i = 2` of the first series is strictly smaller than
-- the corresponding term of the second series
(one_div_pow_strictAnti m1 (n.add_factorial_succ_lt_factorial_add_succ (i := 2) le_rfl))
-- 3. the first series is summable
(remainder_summable m1 n)
-- 4. the second series is summable, since its terms grow quickly
(summable_one_div_pow_of_le m1 fun _ => le_self_add)
-- split the sum in the exponent and massage
_ = ∑' i : ℕ, (1 / m) ^ i * (1 / m ^ (n + 1)!) := by
simp only [pow_add, one_div, mul_inv, inv_pow]
-- factor the constant `(1 / m ^ (n + 1)!)` out of the series
_ = (∑' i, (1 / m) ^ i) * (1 / m ^ (n + 1)!) := tsum_mul_right
_ = (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) := by rw [tsum_geometric_of_lt_one (by positivity) mi]
