Conjugation preserves the multiplicity of a zero

BOTH of the symmetries whose composition ρ ↦ 1 - conj ρ makes the rescaled zeros conjugation-invariant. The conjugation half is the cheap one: it follows from riemannZeta_conj together with the fact that pre- and post-composing with conjugation does not change an analytic order. The reflection half needs the functional equation, and needs the order to be transported across ρ ↦ 1 - ρ, for which Mathlib has nothing ready-made.

The three private lemmas below are adapted, with thanks, from AxiomMath/PrimeNumberTheoremAnd, PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean, where they support the same statement for that project's own order function.

theorem ZetaZeros.zeroMultiplicity_conj {ρ : ℂ} (hρ : ρ ≠ 1) : zeroMultiplicity ((starRingEnd ℂ) ρ) = zeroMultiplicity ρ

Conjugation preserves the multiplicity of a zero.

The functional equation preserves multiplicity

Mathlib has no form of this statement; what it supplies is riemannZeta_one_sub, the functional equation in the form zeta (1 - s) = functionalEqFactor s * zeta s.

Two things then have to be shown, and the second is the real work:

• functionalEqFactor is analytic and NON-VANISHING on the strip. Gamma is non-zero where the real part is positive, the cpow factor is an exp, and cos (pi s / 2) vanishes only at odd integers -- none of which have real part strictly between 0 and 1.
• The order has to move ACROSS the reflection, from rho to 1 - rho. Mathlib has no lemma for that, so analyticOrderAt_comp_const_sub is proved here: the order of w -> f (a - w) at z is the order of f at a - z. It is stated for a general f and a because nothing in it is about zeta, and it is the piece worth reusing.

theorem ZetaZeros.le_analyticOrderAt_comp_const_sub {f : ℂ → ℂ} {a z : ℂ} {n : ℕ} (h : ↑n ≤ analyticOrderAt f (a - z)) : ↑n ≤ analyticOrderAt (fun (w : ℂ) => f (a - w)) z

One direction of the transport of the vanishing order along w ↦ a - w.

theorem ZetaZeros.analyticOrderAt_comp_const_sub (f : ℂ → ℂ) (a z : ℂ) : analyticOrderAt (fun (w : ℂ) => f (a - w)) z = analyticOrderAt f (a - z)

Transport of the vanishing order along an affine reflection.

The factor in the functional equation

noncomputable def ZetaZeros.functionalEqFactor (s : ℂ) : ℂ

The factor in ζ (1 - s) = functionalEqFactor s * ζ s, written with exp rather than cpow so that its analyticity is visible.

Equations

• ZetaZeros.functionalEqFactor s = 2 * Complex.exp (Complex.log (2 * ↑Real.pi) * -s) * Complex.Gamma s * Complex.cos (↑Real.pi * s / 2)

theorem ZetaZeros.two_mul_pi_ne_zero : 2 * ↑Real.pi ≠ 0

theorem ZetaZeros.zeta_one_sub_eq (s : ℂ) (hn : ∀ (n : ℕ), s ≠ -↑n) (h1 : s ≠ 1) : riemannZeta (1 - s) = functionalEqFactor s * riemannZeta s

theorem ZetaZeros.differentiableOn_functionalEqFactor : DifferentiableOn ℂ functionalEqFactor {s : ℂ | 0 < s.re}

theorem ZetaZeros.analyticAt_functionalEqFactor {ρ : ℂ} (h0 : 0 < ρ.re) : AnalyticAt ℂ functionalEqFactor ρ

theorem ZetaZeros.functionalEqFactor_ne_zero {ρ : ℂ} (h0 : 0 < ρ.re) (h1 : ρ.re < 1) : functionalEqFactor ρ ≠ 0

theorem ZetaZeros.zeroMultiplicity_one_sub {ρ : ℂ} (h0 : 0 < ρ.re) (h1 : ρ.re < 1) : zeroMultiplicity (1 - ρ) = zeroMultiplicity ρ

The functional equation preserves multiplicity. For every ρ in the open critical strip, the multiplicity of 1 - ρ as a zero of ζ equals that of ρ.