The Euler-Mascheroni constant γ
#
We define the constant γ
, and give upper and lower bounds for it.
Main definitions and results #
Real.eulerMascheroniConstant
: the constantγ
Real.tendsto_harmonic_sub_log
: the sequencen ↦ harmonic n - log n
tends toγ
asn → ∞
one_half_lt_eulerMascheroniConstant
andeulerMascheroniConstant_lt_two_thirds
: upper and lower bounds.
Outline of proofs #
We show that
- the sequence
eulerMascheroniSeq
given byn ↦ harmonic n - log (n + 1)
is strictly increasing; - the sequence
eulerMascheroniSeq'
given byn ↦ harmonic n - log n
, modified with a junk value forn = 0
, is strictly decreasing; - the difference
eulerMascheroniSeq' n - eulerMascheroniSeq n
is non-negative and tends to 0.
It follows that both sequences tend to a common limit γ
, and we have the inequality
eulerMascheroniSeq n < γ < eulerMascheroniSeq' n
for all n
. Taking n = 6
gives the bounds
1 / 2 < γ < 2 / 3
.
The sequence with n
-th term harmonic n - log (n + 1)
.
Instances For
The sequence with n
-th term harmonic n - log n
. We use a junk value for n = 0
, in order
to have the sequence be strictly decreasing.
Instances For
The Euler-Mascheroni constant γ
.
Instances For
Lower bound for γ
. (The true value is about 0.57.)
Upper bound for γ
. (The true value is about 0.57.)