Sondow scaled positive remainder bound

Proved

EulerMascheroni.Sondow.scaled_integral_bounds

by Yuxuan Xu · Sep 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

euler-mascheroniformalizationsondow

For every positive integer $n$ ,

0<d_{2n}I_n<2^{-n}.

This follows from the established bounds $d_{2n}<8^n$ and $0<I_n<16^{-n}$ . It is a known estimate awaiting formalization.

Preamble

import Definitions.Def_eulerMascheroni_sondow
open EulerMascheroni.Sondow

Formal statement

theorem EulerMascheroni.Sondow.scaled_integral_bounds (n : ℕ) (hn : 0 < n) :
    0 < (d (2*n) : ℝ) * I n ∧ (d (2*n) : ℝ) * I n < (1/2 : ℝ)^n := by sorry

Source

Jonathan Sondow, Criteria for Irrationality of Euler's Constant, https://arxiv.org/pdf/math/0209070 (v2, 4 October 2002). Lemma 3, p. 10.

View graph