Nonvanishing on the line Re s = 1 from a 3-4-1 bound

The classical 3-4-1 argument proves that an L-series does not vanish on the line Re s = 1 in two steps. The first is arithmetic: an Euler product and the positivity of 3 + 4 cos θ + cos 2θ give, for real σ > 1,

1 ≤ ‖L₀(σ) ^ 3 * L₁(σ + it) ^ 4 * L₂(σ + 2it)‖,

where L₀ is the series of the trivial character, L₁ that of a character χ, and L₂ that of χ². The second step is analytic and uses no arithmetic: if L₀(σ) = O((σ - 1)⁻¹) as σ → 1⁺, L₂ stays bounded near 1 + 2it, and L₁ is differentiable at 1 + it and vanishes there, then as σ → 1⁺ the product is O((σ - 1)⁻³ (σ - 1)⁴) = O(σ - 1), contradicting the lower bound. This file proves the second step for arbitrary functions, so that each family of L-series needs to supply only its own 3-4-1 bound and its analytic inputs.

The growth condition on f₀ is the one-sided bound f₀(σ) = O((σ - 1)⁻¹) as real σ → 1⁺. It follows from a limit of (σ - 1) f₀(σ) as σ → 1⁺, which is how such a bound is usually available for a Dedekind zeta function; TauCeti.isBigO_inv_sub_one_of_tendsto_sub_one_mul records that implication.

Main results

• TauCeti.LSeries.ne_zero_of_threeFourOne: the 3-4-1 bound together with the bound f₀(σ) = O((σ - 1)⁻¹), differentiability of f₁ at 1 + it and continuity of f₂ at 1 + 2it forces f₁ (1 + it) ≠ 0.

References

• H. Davenport, Multiplicative Number Theory, Chapter 4.
• The argument is the one in Mathlib's Mathlib/NumberTheory/LSeries/Nonvanishing.lean, by Michael Stoll and David Loeffler, where the private lemma DirichletCharacter.LFunction_ne_zero_of_not_quadratic_or_ne_one carries it out for Dirichlet L-functions. Here it is separated from the Dirichlet characters.

theorem TauCeti.LSeries.ne_zero_of_threeFourOne {f₀ f₁ f₂ : ℂ → ℂ} {t : ℝ} (hbound : ∀ᶠ (σ : ℝ) in nhdsWithin 1 (Set.Ioi 1), 1 ≤ ‖f₀ ↑σ ^ 3 * f₁ (↑σ + Complex.I * ↑t) ^ 4 * f₂ (↑σ + 2 * Complex.I * ↑t)‖) (h₀ : (fun (σ : ℝ) => f₀ ↑σ) =O[nhdsWithin 1 (Set.Ioi 1)] fun (σ : ℝ) => (σ - 1)⁻¹) (h₁ : DifferentiableAt ℂ f₁ (1 + Complex.I * ↑t)) (h₂ : ContinuousAt f₂ (1 + 2 * Complex.I * ↑t)) : f₁ (1 + Complex.I * ↑t) ≠ 0

The 3-4-1 nonvanishing criterion. Let f₀, f₁, f₂ be complex functions and t real. Suppose that, as σ → 1⁺ through real values,

• 1 ≤ ‖f₀(σ) ^ 3 * f₁(σ + it) ^ 4 * f₂(σ + 2it)‖ eventually;
• f₀(σ) = O((σ - 1)⁻¹);

and that f₁ is complex differentiable at 1 + it and f₂ is continuous at 1 + 2it. Then f₁ (1 + it) ≠ 0.

The bound is the one an Euler product and 3 + 4 cos θ + cos 2θ ≥ 0 give when f₀, f₁, f₂ are the series of the trivial character, of a character χ, and of χ²; the analytic hypotheses are where a continuation of these series across Re s = 1 is used.