Riemann xi function

DefinitionRiemann xi function#✓fully proved

Let \(\Lambda\) be the completed Riemann zeta function, the meromorphic continuation of \(\pi^{-s/2}\Gamma(s/2)\zeta(s)\), which has simple poles at \(s = 0\) and \(s = 1\), and let \(\Lambda_0\) be the entire function with \(\Lambda_0(s) = \Lambda(s) + \frac{1}{s} + \frac{1}{1 - s}\) for \(s \ne 0, 1\). The Riemann xi function is \(\xi(s) = \frac{s(s - 1)}{2}\Lambda_0(s) + \frac{1}{2}\) for \(s \in \mathbb{C}\).

noncomputable def riemannXi (s : ℂ) : ℂ :=
  s * (s - 1) / 2 * completedRiemannZeta₀ s + 1 / 2

Used by 8

Used byThe Riemann xi function is entire · Zeros of the xi function have real part less than one · Zeros of the xi function have positive real part · Basic properties of the Riemann xi function · The xi function in terms of the completed zeta function · Zeros of the xi function lie in the critical strip · The xi function has no zeros with real part at least one · Functional equation of the Riemann xi function

TheoremThe Riemann xi function is entire#✓fully proved

The Riemann xi function \(\xi\) is complex differentiable at every point of \(\mathbb{C}\).

theorem differentiable_riemannXi : Differentiable ℂ riemannXi

Uses 1 · Used by 1

Statement usesRiemann xi function

Used byBasic properties of the Riemann xi function

TheoremFunctional equation of the Riemann xi function#✓fully proved

Let \(\xi\) be the Riemann xi function. For every complex number \(s\), \(\xi(1 - s) = \xi(s)\).

theorem riemannXi_one_sub (s : ℂ) : riemannXi (1 - s) = riemannXi s

Uses 1 · Used by 2

Statement usesRiemann xi function

Used byZeros of the xi function have positive real part · Basic properties of the Riemann xi function

TheoremThe xi function in terms of the completed zeta function#✓fully proved

Let \(\xi\) be the Riemann xi function and let \(\Lambda\) be the completed Riemann zeta function, the meromorphic continuation of \(\pi^{-s/2}\Gamma(s/2)\zeta(s)\), which has simple poles at \(s = 0\) and \(s = 1\). For every complex number \(s\) with \(s \ne 0\) and \(s \ne 1\), \(\xi(s) = \frac{s(s - 1)}{2}\Lambda(s)\).

theorem riemannXi_eq_mul_completedRiemannZeta {s : ℂ} (hs0 : s ≠ 0)
    (hs1 : s ≠ 1) :
    riemannXi s = s * (s - 1) / 2 * completedRiemannZeta s

Uses 1 · Used by 1

Statement usesRiemann xi function

Used byThe xi function has no zeros with real part at least one

TheoremThe xi function has no zeros with real part at least one#✓fully proved

Let \(\xi\) be the Riemann xi function. For every complex number \(s\) with \(\operatorname{Re}(s) \ge 1\), \(\xi(s) \ne 0\).

theorem riemannXi_ne_zero_of_one_le_re {s : ℂ} (hs : 1 ≤ s.re) :
    riemannXi s ≠ 0

Uses 2 · Used by 2

Statement usesRiemann xi function

Proof usesThe xi function in terms of the completed zeta function

Used byZeros of the xi function have real part less than one · Zeros of the xi function have positive real part

TheoremZeros of the xi function have positive real part#✓fully proved

Let \(\xi\) be the Riemann xi function. If \(s\) is a complex number with \(\xi(s) = 0\), then \(\operatorname{Re}(s) > 0\).

theorem re_pos_of_riemannXi_eq_zero {s : ℂ} (h : riemannXi s = 0) :
    0 < s.re

Uses 3 · Used by 1

Statement usesRiemann xi function

Proof usesThe xi function has no zeros with real part at least one · Functional equation of the Riemann xi function

Used byZeros of the xi function lie in the critical strip

TheoremZeros of the xi function have real part less than one#✓fully proved

Let \(\xi\) be the Riemann xi function. If \(s\) is a complex number with \(\xi(s) = 0\), then \(\operatorname{Re}(s) < 1\).

theorem re_lt_one_of_riemannXi_eq_zero {s : ℂ} (h : riemannXi s = 0) :
    s.re < 1

Uses 2 · Used by 1

Statement usesRiemann xi function

Proof usesThe xi function has no zeros with real part at least one

Used byZeros of the xi function lie in the critical strip

TheoremZeros of the xi function lie in the critical strip#✓fully proved

Let \(\xi\) be the Riemann xi function. If \(s\) is a complex number with \(\xi(s) = 0\), then \(0 < \operatorname{Re}(s) < 1\).

theorem riemannXi_mem_strip {s : ℂ} (h : riemannXi s = 0) :
    0 < s.re ∧ s.re < 1

Uses 3 · Used by 1

Statement usesRiemann xi function

Proof usesZeros of the xi function have real part less than one · Zeros of the xi function have positive real part

Used byBasic properties of the Riemann xi function

TheoremBasic properties of the Riemann xi function#✓fully proved

The Riemann xi function \(\xi\) is entire, satisfies \(\xi(1 - s) = \xi(s)\) for every complex number \(s\), and every complex number \(s\) with \(\xi(s) = 0\) satisfies \(0 < \operatorname{Re}(s) < 1\).

theorem riemannXi_entire_functional_equation_and_critical_strip :
    Differentiable ℂ riemannXi ∧
      (∀ s : ℂ, riemannXi (1 - s) = riemannXi s) ∧
      ∀ s : ℂ, riemannXi s = 0 → 0 < s.re ∧ s.re < 1

Uses 4

Statement usesRiemann xi function

Proof usesThe Riemann xi function is entire · Zeros of the xi function lie in the critical strip · Functional equation of the Riemann xi function

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.