The 3-4-1 positivity combination

This file packages the elementary positivity input in the classical 3-4-1 argument for nonvanishing of Dirichlet series. For a phase z on the complex unit circle,

3 + 4 Re(z) + Re(z²) = 2 (1 + Re(z))² ≥ 0.

The weights 3, 4, and 1 are nonnegative. We record their expression as a finite nonnegative trigonometric combination and prove the corresponding inequality for logarithms of Euler factors. These results contain no continuation, nonvanishing, or character-specific hypotheses; downstream applications provide those analytic inputs separately.

Main declarations

• TauCeti.LSeries.isNonnegativeTrigonometricCombination_threeFourOne packages the frequencies 0, 1, and 2 with weights 3, 4, and 1.
• TauCeti.LSeries.threeFourOne_re_neg_log_one_sub_nonneg is the corresponding inequality for logarithms of Euler factors in the open unit disk.

Provenance

The 3-4-1 argument is classical; see Davenport, Multiplicative Number Theory, Chapter 4. The logarithmic form specializes the private lemma DirichletCharacter.re_log_comb_nonneg' in Mathlib's Mathlib/NumberTheory/LSeries/Nonvanishing.lean, by Michael Stoll and David Loeffler, through TauCeti.sum_re_neg_log_one_sub_nonneg.

The concrete 3-4-1 combination

def TauCeti.LSeries.threeFourOneWeight : Fin 3 → ℝ

The three nonnegative weights 3, 4, and 1 in the 3-4-1 combination.

Equations

• TauCeti.LSeries.threeFourOneWeight = ![3, 4, 1]

def TauCeti.LSeries.threeFourOneFrequency : Fin 3 → ℕ

The frequencies 0, 1, and 2 in the 3-4-1 combination.

Equations

• TauCeti.LSeries.threeFourOneFrequency = ![0, 1, 2]

def TauCeti.LSeries.threeFourOneCombination (z : ℂ) : ℝ

The 3-4-1 trigonometric expression evaluated at a complex phase.

Equations

• TauCeti.LSeries.threeFourOneCombination z = 3 + 4 * z.re + (z ^ 2).re

@[simp]

theorem TauCeti.LSeries.threeFourOneWeight_zero : threeFourOneWeight 0 = 3

The first 3-4-1 weight is 3.

@[simp]

theorem TauCeti.LSeries.threeFourOneWeight_one : threeFourOneWeight 1 = 4

The second 3-4-1 weight is 4.

@[simp]

theorem TauCeti.LSeries.threeFourOneWeight_two : threeFourOneWeight 2 = 1

The third 3-4-1 weight is 1.

@[simp]

theorem TauCeti.LSeries.threeFourOneFrequency_zero : threeFourOneFrequency 0 = 0

The first 3-4-1 frequency is 0.

@[simp]

theorem TauCeti.LSeries.threeFourOneFrequency_one : threeFourOneFrequency 1 = 1

The second 3-4-1 frequency is 1.

@[simp]

theorem TauCeti.LSeries.threeFourOneFrequency_two : threeFourOneFrequency 2 = 2

The third 3-4-1 frequency is 2.

theorem TauCeti.LSeries.threeFourOneCombination_def (z : ℂ) : threeFourOneCombination z = 3 + 4 * z.re + (z ^ 2).re

The defining formula for threeFourOneCombination.

@[simp]

theorem TauCeti.LSeries.trigonometricCombination_threeFourOne (z : ℂ) : trigonometricCombination Finset.univ threeFourOneWeight threeFourOneFrequency z = threeFourOneCombination z

The abstract finite combination with 3-4-1 weights is the usual concrete expression.

theorem TauCeti.LSeries.threeFourOneCombination_eq_two_mul_sq {z : ℂ} (hz : ‖z‖ = 1) : threeFourOneCombination z = 2 * (z.re + 1) ^ 2

On the unit circle the 3-4-1 expression is twice a square.

theorem TauCeti.LSeries.isNonnegativeTrigonometricCombination_threeFourOne : IsNonnegativeTrigonometricCombination Finset.univ threeFourOneWeight threeFourOneFrequency

The weights and frequencies of the 3-4-1 expression form a finite nonnegative trigonometric combination.

theorem TauCeti.LSeries.threeFourOneCombination_nonneg {z : ℂ} (hz : ‖z‖ ≤ 1) : 0 ≤ threeFourOneCombination z

The 3-4-1 expression is nonnegative on the closed complex unit disk.

Euler-factor form

theorem TauCeti.LSeries.threeFourOne_re_neg_log_one_sub_nonneg {a : ℝ} (ha₀ : 0 ≤ a) (ha₁ : a < 1) {z : ℂ} (hz : ‖z‖ ≤ 1) : 0 ≤ 3 * (-Complex.log (1 - ↑a)).re + 4 * (-Complex.log (1 - ↑a * z)).re + (-Complex.log (1 - ↑a * z ^ 2)).re

The 3-4-1 inequality for logarithms of three Euler factors in the open unit disk.