TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-14

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Euler–Mascheroni constant and the harmonic asymptotic

Statement

For $n \geq 1$ , let

$H_{n} = \sum_{k = 1}^{n} \frac{1}{k}, γ_{n} = H_{n} - \log n .$

The sequence $(γ_{n})$ is strictly decreasing and is bounded below by $1 - \log 2$ . It therefore converges to a constant $γ$ satisfying $0 < γ < 1$ , and

$H_{n} = \log n + γ + o (1) .$

Consequently, $H_{n} / \log n \to 1$ as $n \to \infty$ , with the quotient considered for $n \geq 2$ .

Facts & Assumptions

Given: The sequences $(H_{n})$ and $(γ_{n})$ displayed in the statement.

[A1]

For every $n \geq 1$ , $H_{n} = \sum_{k = 1}^{n} 1 / k$ and $γ_{n} = H_{n} - \log n$ .

[L1]

For $x > 0$ , $\log x = \int_{1}^{x} d t / t$ , and the derivative of $\log$ is $1 / x$ (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t).

[L2]

Let $a < b$ and let $f, g : [a, b] \to R$ be integrable. If $f (x) \geq 0$ for every $x \in [a, b]$ , then $\int_{a}^{b} f \geq 0$ ; if $f (x) \leq g (x)$ for every $x \in [a, b]$ , then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and if $m \leq f (x) \leq M$ for every $x \in [a, b]$ , with $m, M$ real, then $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ (If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ ).

[L3]

If $a < c < b$ , then a bounded function on $[a, b]$ is integrable there exactly when its restrictions to $[a, c]$ and $[c, b]$ are integrable, and in that case $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ (For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ ).

[L4]

Every nonincreasing real sequence that is bounded below converges to its infimum (A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum).

Proof

technique · direct

1.1

For every $n \geq 1$ , $γ_{n + 1} - γ_{n} = 1 / (n + 1) - \int_{n}^{n + 1} d t / t$ .

A1L1L3algebra

1.2

Splitting the integral at $n + 1 / 2$ gives $\int_{n}^{n + 1} d t / t \geq (1 / 2) / (n + 1 / 2) + (1 / 2) / (n + 1) > 1 / (n + 1)$ .

L2L3algebra

1.3

If $n \geq 2$ , additivity and $1 / t \leq 1 / k$ on $[k, k + 1]$ give $\log n = \log 2 + \sum_{k = 2}^{n - 1} \int_{k}^{k + 1} d t / t \leq \log 2 + \sum_{k = 2}^{n - 1} 1 / k$ , where the sum is empty when $n = 2$ ; thus $γ_{n} \geq 1 - \log 2 + 1 / n > 1 - \log 2$ .

A1L1L2L3algebra

1.4

Splitting $[1, 2]$ at $3 / 2$ gives $\log 2 = \int_{1}^{2} d t / t \leq 1 / 2 + 1 / 3 = 5 / 6 < 1$ ; in particular, $γ_{1} = 1 \geq 1 - \log 2 > 0$ .

A1L1L2L3algebra

1.5

For every integer $m \geq 1$ , splitting $[1, 2^{m}]$ into $[2^{j}, 2^{j + 1}]$ gives $\log (2^{m}) = \sum_{j = 0}^{m - 1} \int_{2^{j}}^{2^{j + 1}} d t / t \geq \sum_{j = 0}^{m - 1} 1 / 2 = m / 2$ .

L1L2L3algebra

2.1

Hence $γ_{n + 1} < γ_{n}$ for every $n \geq 1$ .

step 1.1step 1.2algebra

2.2

Therefore $γ_{n} \geq 1 - \log 2$ for every $n \geq 1$ .

step 1.3step 1.4

2.3

It follows that $\log n \to \infty$ . Let $m \geq 1$ and $n \geq 2^{m}$ . If $n = 2^{m}$ then $\log n = \log (2^{m})$ . If $n > 2^{m}$ then $1 < 2^{m} < n$ , so $\log n = \int_{1}^{n} d t / t = \int_{1}^{2^{m}} d t / t + \int_{2^{m}}^{n} d t / t = \log (2^{m}) + \int_{2^{m}}^{n} d t / t$ , and $1 / t \geq 0$ on $[2^{m}, n]$ makes that last integral nonnegative. Either way $\log n \geq \log (2^{m}) \geq m / 2$ .

L1L2L3step 1.5algebra

3.1

By monotone convergence, there is a real number $γ$ such that $γ_{n} \to γ$ .

L4step 2.1step 2.2

3.2

The lower bound and strict decrease give $0 < γ_{n} \leq γ_{1} = 1$ for every $n \geq 1$ .

step 1.4step 2.1step 2.2

4.1

Since $γ$ is the infimum of the $γ_{n}$ , $γ \geq 1 - \log 2 > 0$ ; and since the sequence is strictly decreasing, $γ \leq γ_{2} < γ_{1} = 1$ . Hence $0 < γ < 1$ .

step 1.4step 2.1step 2.2step 3.1algebra

4.2

The identity $H_{n} = \log n + γ_{n}$ and the convergence $γ_{n} \to γ$ give $H_{n} = \log n + γ + (γ_{n} - γ) = \log n + γ + o (1)$ .

A1step 3.1algebra

4.3

Consequently, $γ_{n} / \log n \to 0$ as $n \to \infty$ .

step 2.3step 3.2algebra

5.1

Finally, for $n \geq 2$ , $H_{n} / \log n = 1 + γ_{n} / \log n \to 1$ .

A1step 4.3algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 86 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

W. F. Trench, Introduction to Real Analysis, Exercise 4.3.14 (standard reference, not scraped)