The 3-4-1 bound for the Euler products of unitary ideal weights

Let χ be a unitary ideal weight of a number field K, and let χ₀ be a weight that is trivial on its good ideals and whose bad primes are among those of χ — for instance the trivial weight, whose L-series is the Dedekind zeta function ζ_K. For real σ > 1 and real t, this file proves the classical 3-4-1 inequality

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

where each L-series is the LSeries of the norm coefficients of the weight. It is the positivity input for nonvanishing on the line Re s = 1, and is exactly the bound hypothesis of the analytic criterion TauCeti.LSeries.ne_zero_of_threeFourOne: a continuation of L(χ, ·) that is differentiable at 1 + it does not vanish there, provided L(χ₀, σ) = O((σ - 1)⁻¹) as σ → 1⁺ and L(χ², ·) continues continuously to 1 + 2it.

Main results

• TauCeti.UnitaryIdealWeight.norm_LSeries_threeFourOne_ge_one: the 3-4-1 bound for a unitary weight χ against a weight χ₀ trivial on its good ideals, with bad primes among those of χ.
• TauCeti.UnitaryIdealWeight.norm_dedekindZeta_threeFourOne_ge_one: the case χ₀ = 1, where the first factor is the Dedekind zeta function.
• TauCeti.UnitaryIdealWeight.ne_zero_of_eqOn_LSeries: the resulting nonvanishing criterion on the line Re s = 1, for continuations of the L-series of χ and of χ².

References

• H. Davenport, Multiplicative Number Theory, Chapter 4.
• The global argument is that of Mathlib's DirichletCharacter.norm_LSeries_product_ge_one in Mathlib/NumberTheory/LSeries/Nonvanishing.lean, by Michael Stoll and David Loeffler, with unitary ideal weights of a number field in place of Dirichlet characters.

theorem TauCeti.UnitaryIdealWeight.norm_LSeries_threeFourOne_ge_one {K : Type u_1} [Field K] [NumberField K] {χ₀ : MultiplicativeIdealWeight K} (χ : UnitaryIdealWeight K) (h₀ : χ₀.IsTrivialOnGood) (hbad : χ₀.badPrimes ⊆ (↑χ).badPrimes) {σ : ℝ} (hσ : 1 < σ) (t : ℝ) : 1 ≤ ‖LSeries ⇑((normCoeff K) χ₀.toIdealArithmeticFunction) ↑σ ^ 3 * LSeries (⇑((normCoeff K) χ.toIdealArithmeticFunction)) (↑σ + Complex.I * ↑t) ^ 4 * LSeries (⇑((normCoeff K) (χ ^ 2).toIdealArithmeticFunction)) (↑σ + 2 * Complex.I * ↑t)‖

The 3-4-1 bound for unitary ideal weights. Let χ be a unitary weight and χ₀ a weight that is trivial on its good ideals, with every bad prime of χ₀ a bad prime of χ. For real σ > 1 and real t, the L-series of χ₀ at σ cubed, times that of χ at σ + it to the fourth power, times that of χ² at σ + 2it, has norm at least one.

theorem TauCeti.UnitaryIdealWeight.norm_dedekindZeta_threeFourOne_ge_one {K : Type u_1} [Field K] [NumberField K] (χ : UnitaryIdealWeight K) {σ : ℝ} (hσ : 1 < σ) (t : ℝ) : 1 ≤ ‖NumberField.dedekindZeta K ↑σ ^ 3 * LSeries (⇑((normCoeff K) χ.toIdealArithmeticFunction)) (↑σ + Complex.I * ↑t) ^ 4 * LSeries (⇑((normCoeff K) (χ ^ 2).toIdealArithmeticFunction)) (↑σ + 2 * Complex.I * ↑t)‖

The 3-4-1 bound against the Dedekind zeta function. For every unitary weight χ, real σ > 1 and real t, 1 ≤ ‖ζ_K(σ) ^ 3 * L(χ, σ + it) ^ 4 * L(χ², σ + 2it)‖.

theorem TauCeti.UnitaryIdealWeight.ne_zero_of_eqOn_LSeries {K : Type u_1} [Field K] [NumberField K] (χ : UnitaryIdealWeight K) {s : ℂ} (hs : s.re = 1) {f f₂ : ℂ → ℂ} (hf : DifferentiableAt ℂ f s) (hfL : Set.EqOn f (LSeries ⇑((normCoeff K) χ.toIdealArithmeticFunction)) {z : ℂ | 1 < z.re}) (hf₂ : ContinuousAt f₂ (2 * s - 1)) (hf₂L : Set.EqOn f₂ (LSeries ⇑((normCoeff K) (χ ^ 2).toIdealArithmeticFunction)) {z : ℂ | 1 < z.re}) : f s ≠ 0

The 3-4-1 nonvanishing criterion for a unitary weight. Let χ be a unitary weight and s a point with Re s = 1. If f is complex differentiable at s and f₂ is continuous at 2s - 1, and they agree on Re z > 1 with the L-series of χ and of its pointwise square χ² respectively, then f s ≠ 0.