Documentation

Mathlib.NumberTheory.Harmonic.EulerMascheroni

The Euler-Mascheroni constant γ #

We define the constant γ, and give upper and lower bounds for it.

Main definitions and results #

Outline of proofs #

We show that

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
Instances For
    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
    Instances For

      The Euler-Mascheroni constant γ.

      Equations
      Instances For

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

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