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 sequence n ↦ harmonic n - log n tends to γ as n → ∞
• one_half_lt_eulerMascheroniConstant and eulerMascheroniConstant_lt_two_thirds: upper and lower bounds.

Outline of proofs

We show that

• the sequence eulerMascheroniSeq given by n ↦ harmonic n - log (n + 1) is strictly increasing;
• the sequence eulerMascheroniSeq' given by n ↦ harmonic n - log n, modified with a junk value for n = 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.

noncomputable def Real.eulerMascheroniSeq (n : ℕ) : ℝ

The sequence with n-th term harmonic n - log (n + 1).

Equations

• Real.eulerMascheroniSeq n = ↑(harmonic n) - Real.log (↑n + 1)

theorem Real.eulerMascheroniSeq_zero : eulerMascheroniSeq 0 = 0

theorem Real.strictMono_eulerMascheroniSeq : StrictMono eulerMascheroniSeq

theorem Real.one_half_lt_eulerMascheroniSeq_six : 1 / 2 < eulerMascheroniSeq 6

noncomputable def Real.eulerMascheroniSeq' (n : ℕ) : ℝ

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.

Equations

• Real.eulerMascheroniSeq' n = if n = 0 then 2 else ↑(harmonic n) - Real.log ↑n

theorem Real.eulerMascheroniSeq'_one : eulerMascheroniSeq' 1 = 1

theorem Real.strictAnti_eulerMascheroniSeq' : StrictAnti eulerMascheroniSeq'

theorem Real.eulerMascheroniSeq'_six_lt_two_thirds : eulerMascheroniSeq' 6 < 2 / 3

theorem Real.eulerMascheroniSeq_lt_eulerMascheroniSeq' (m n : ℕ) : eulerMascheroniSeq m < eulerMascheroniSeq' n

noncomputable def Real.eulerMascheroniConstant : ℝ

The Euler-Mascheroni constant γ.

Equations

• Real.eulerMascheroniConstant = limUnder Filter.atTop Real.eulerMascheroniSeq

theorem Real.tendsto_eulerMascheroniSeq : Filter.Tendsto eulerMascheroniSeq Filter.atTop (nhds eulerMascheroniConstant)

theorem Real.tendsto_harmonic_sub_log_add_one : Filter.Tendsto (fun (n : ℕ) => ↑(harmonic n) - log (↑n + 1)) Filter.atTop (nhds eulerMascheroniConstant)

theorem Real.tendsto_eulerMascheroniSeq' : Filter.Tendsto eulerMascheroniSeq' Filter.atTop (nhds eulerMascheroniConstant)

theorem Real.tendsto_harmonic_sub_log : Filter.Tendsto (fun (n : ℕ) => ↑(harmonic n) - log ↑n) Filter.atTop (nhds eulerMascheroniConstant)

theorem Real.eulerMascheroniSeq_lt_eulerMascheroniConstant (n : ℕ) : eulerMascheroniSeq n < eulerMascheroniConstant

theorem Real.eulerMascheroniConstant_lt_eulerMascheroniSeq' (n : ℕ) : eulerMascheroniConstant < eulerMascheroniSeq' n

theorem Real.one_half_lt_eulerMascheroniConstant : 1 / 2 < eulerMascheroniConstant

Lower bound for γ. (The true value is about 0.57.)

theorem Real.eulerMascheroniConstant_lt_two_thirds : eulerMascheroniConstant < 2 / 3

Upper bound for γ. (The true value is about 0.57.)