Euler-Mascheroni constant and results.

1 Euler’s constant in infinite sum form. (Sondow (2005).)

(Note: The index of the inner summand in the Lean definition is shifted by one so the series can be expressed as a sum from \(n=0\) to \(\infty \) (so we can use "tsum" for cleaner proof).)

Lemma 1 Nonnegativity of the inner sum
✓
#

Lean declarations

For every integer \(n \ge 1\),

\[ \frac{1}{n} - \ln {\frac{n+1}{n}} \ge 0. \]
Proof ▶

The inequality \(\ln x \le x-1\) holds for all \(x {\gt} 0\). Taking \(x=\frac{n+1}{n}\) gives

\[ \ln {\frac{n+1}{n}} \le \frac{n+1}{n}-1 = \frac{1}{n}. \]

Rearranging yields the stated nonnegativity.

Lemma 2 Partial sum of the infinite sum
✓
#

Lean declarations

For every integer \(N \ge 1\),

\[ \sum _{n=1}^{N}\left(\frac{1}{n} - \ln {\frac{n+1}{n}}\right) = H_{N} - \ln {\left(N+1\right)}, \]

where \(H_{N}=\sum _{n=1}^N \frac{1}{n}\) is the \(N\)-th harmonic number.

Proof ▶

Split the sum:

\[ \sum _{n=1}^{N}\frac{1}{n} - \sum _{n=1}^{N}\ln {\frac{n+1}{n}}. \]

The first term is \(H_{N}\). The second term telescopes:

\[ \sum _{n=1}^{N}\left(\ln {n+1}-\ln n\right)=\ln {\left(N+1\right)}-\ln 1=\ln {\left(N+1\right)}. \]

Combining gives the claimed identity.

Theorem 3 Upper bound of the sum
✓
#

Lean declarations

For every integer \(N \ge 1\),

\[ \sum _{n=1}^{N}\left(\frac{1}{n} - \ln {\frac{n+1}{n}}\right) \leq 1 \]
Proof ▶

We use the results from the previous lemma, and get the sum as \(H_N - \ln {N + 1}\). This is the same as mathlib’s "Real.eulerMascheroniSeq" we can use the results from mathlib. (Alternately, we can use the fact that the upper bound of \(\gamma \) is \(2/3\) and \(\gamma {\lt} H_{N} - \ln {N+1}\) to get a stricter results?)

Theorem 4 Sondow 2005 (2) (Infinite sum)
✓
#

Lean declarations

\[ \gamma = \lim _{n \to \infty }{\left(H_{n} - \ln n\right)} = \sum _{n=1}^{\infty }\left(\frac{1}{n} - \ln {\frac{n+1}{n}}\right). \]
Proof ▶

By combining all of the previous results (plus the fact that \(H_n - \ln {n+1}\) that we got from partial sum is basically the same as mathlib’s one), we can conclude that the infinite sum is equal to \(\lim _{n \to \infty }\left(H_{n} - \ln n\right)\)