Euler-Mascheroni constant

Stream: Is there code for X?

[Michael Stoll]

Is the Euler-Mascheroni constant $\gamma = \lim_{N \to \infty} \sum_{n=1}^N \frac{1}{n} - \log N$ defined somewhere in Mathlib?

[Yury G. Kudryashov]

Probably, no: @loogle tsum, Real.log

[loogle]

:shrug: nothing found

[Terence Tao]

Are there any properties would you like to have about $\gamma$ beyond its mere existence? I started a project to obtain elementary estimates on sums of slowly varying functions which would eventually give things like this, but it's only in its early stages right now ( https://github.com/teorth/asymptotic ).

[Terence Tao]

In particular, I aim to show that $\sum_{n \in I \cap {\mathbb Z}} f(n) = \int_I f(t)\ dt + O( |f(a)| + \int_I |f'(t)|\ dt )$ whenever $f \in C^1(I)$ for some interval $I$ and $a$ is an element of $I$, which is a useful estimate for estimating things like sums of $1/n^s$, $\log n$, etc..

[Terence Tao]

The unit fractions project may possibly already have this constant though, since they worked out Mertens' theorem. Let me check

[Eric Rodriguez]

It does, bhavik mentioned it.

[Terence Tao]

Found it at https://github.com/b-mehta/unit-fractions//blob/b60c39a3ebd40a84104a4064840b10fc2af15fb8/src/for_mathlib/basic_estimates.lean#L282

[Terence Tao]

I guess we should ping @Bhavik Mehta or @Thomas Bloom for the current status of this code (e.g., if it has been ported to Lean4 and/or Mathlib)

[Michael Stoll]

I'm trying to formalize the reduction of PNT to Wiener-Ikehara. The Euler-Mascheroni constant comes up like this:

import Mathlib

open BigOperators in
/-- The *Euler-Mascheroni Constant*, also equal to the limit of `∑ n < N, 1/n - log N`. -/
noncomputable
def γ : ℝ := ∫ x in Set.Ici (1 : ℝ), 1 / ⌊x⌋ - 1 / x

/-- The negative logarithmic derivative of the Riemann zeta function with a term added
to cancel the simple pole at `z = 1`. -/
noncomputable
def F (z : ℂ) : ℂ := if z = 1 then (-γ) else -deriv riemannZeta z / riemannZeta z - 1 / (z - 1)

lemma continuousOn_F : ContinuousOn F {z | z = 1 ∨ riemannZeta z ≠ 0} := by sorry

Of course, one only needs that one can fill in the singularity of F with some value.

[Terence Tao]

If you already have meromorphic continuation of zeta around 1, and that zeta has a simple pole at 1, then one can get the existence of the constant from pure complex analysis.

[Terence Tao]

e.g., from the removable singularity theorem https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Complex/RemovableSingularity.html

[Terence Tao]

Huh. I'm not seeing much support for meromorphic functions in Mathlib.

[Terence Tao]

But the analyticity and non-zero nature of the completed zeta function at s=1 should be enough.

[Terence Tao]

Indeed, one should be able to rewrite -deriv riemannZeta z / riemannZeta z - 1 / (z - 1) as negative the log derivative of fun z ↦ (Λ z) * (z-1) plus some terms that are easily seen to be analytic at z=1, and the analyticity of the renormalized completed zeta function Λ₀ guarantees that (Λ z) * (z-1)is analytic and non-zero at z=1, and that suffices.

[Junyan Xu]

Meromorphic functions were last discussed here, but there has been no further PR since #7456 ...

[Terence Tao]

I guess one doesn't strictly speaking need a theory of memomorphic functions in order to have Laurent expansions around isolated singularities and the residue theorem (say for rectangular contours), which is what would be needed for analytic number theory applications.

[Yaël Dillies]

@Bhavik Mehta has it in unit-fractions Damn, I was too slow!

[David Loeffler]

Junyan Xu said:

Meromorphic functions were last discussed here, but there has been no further PR since #7456 ...

Yeah, I got side-tracked a bit on that one, sorry! I will dig up the code I wrote (definition of "meromorphic") and PR it.

[David Loeffler]

David Loeffler said:

Junyan Xu said:

Meromorphic functions were last discussed here, but there has been no further PR since #7456 ...

Yeah, I got side-tracked a bit on that one, sorry! I will dig up the code I wrote (definition of "meromorphic") and PR it.

I failed to dig up the code (I think I must have git stash-ed it and then deleted that git checkout without realising it was there). Anyway, I've reconstructed the first chunk of it at #9590, which defines what it means for f to be MeromorphicAt a specific point.