noncomputable def AnalyticNumberTheory.LargeSieve.TatuzawaMultiplicativeTransfer.pairCharacter {q₁ q₂ : ℕ} (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) : DirichletCharacter ℂ (q₁ * q₂)

The common-level product of two characters of possibly different primitive levels. Its natural-number values are the pointwise products of the original characters; the common level is used only to package that product as a Dirichlet character.

Equations

• AnalyticNumberTheory.LargeSieve.TatuzawaMultiplicativeTransfer.pairCharacter χ₁ χ₂ = (DirichletCharacter.changeLevel ⋯) χ₁ * (DirichletCharacter.changeLevel ⋯) χ₂

theorem AnalyticNumberTheory.LargeSieve.TatuzawaMultiplicativeTransfer.pairCharacter_apply {q₁ q₂ : ℕ} (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) (n : ℕ) : (pairCharacter χ₁ χ₂) ↑n = χ₁ ↑n * χ₂ ↑n

theorem AnalyticNumberTheory.LargeSieve.TatuzawaMultiplicativeTransfer.pairCharacter_square_eq_one {q₁ q₂ : ℕ} (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) (h₁ : χ₁ ^ 2 = 1) (h₂ : χ₂ ^ 2 = 1) : pairCharacter χ₁ χ₂ ^ 2 = 1

theorem AnalyticNumberTheory.LargeSieve.TatuzawaMultiplicativeTransfer.datum_eq_of_pairCharacter_eq_one (x y : PrimitiveQuadraticDatum) (hpair : pairCharacter x.character y.character = 1) : x = y

If the common-level product of two primitive quadratic characters is principal, then the two primitive data are identical. This is the dependent bookkeeping needed before applying a distinct-character value-product bound: the proof first recovers both divisibilities of the primitive levels from factorsThrough_gcd, and only then transports the character equality across the resulting equality of levels.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaMultiplicativeTransfer.pairCharacter_ne_one_of_datum_ne (x y : PrimitiveQuadraticDatum) (hxy : x ≠ y) : pairCharacter x.character y.character ≠ 1

Distinct primitive quadratic data have a nonprincipal common-level product.

noncomputable def AnalyticNumberTheory.LargeSieve.TatuzawaMultiplicativeTransfer.pairValue (x y : PrimitiveQuadraticDatum) : ℝ

The real value at one of the common-level product character.

Equations

• AnalyticNumberTheory.LargeSieve.TatuzawaMultiplicativeTransfer.pairValue x y = (DirichletCharacter.LFunction (AnalyticNumberTheory.LargeSieve.TatuzawaMultiplicativeTransfer.pairCharacter x.character y.character) 1).re

theorem AnalyticNumberTheory.LargeSieve.TatuzawaMultiplicativeTransfer.pairValue_pos_of_datum_ne (x y : PrimitiveQuadraticDatum) (hxy : x ≠ y) : 0 < pairValue x y

The product character of distinct primitive quadratic data has a strictly positive value at one. This is the first value-at-one input supplied by the four-factor Euler product, rather than by an exception predicate.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaMultiplicativeTransfer.fourFactor_nonZetaValueProductAtOne_pos (x y : PrimitiveQuadraticDatum) (hxy : x ≠ y) : 0 < x.value * y.value * pairValue x y

All three non-zeta values in the four-factor product are positive at one for distinct primitive quadratic data.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaMultiplicativeTransfer.fourFactorEulerCoefficient_nonneg {q₁ q₂ : ℕ} (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) (h₁ : χ₁ ^ 2 = 1) (h₂ : χ₂ ^ 2 = 1) (n : ℕ) : 0 ≤ 1 + χ₁ ↑n + χ₂ ↑n + (pairCharacter χ₁ χ₂) ↑n

The local Euler coefficient for ζ(s)L(s,χ₁)L(s,χ₂)L(s,χ₁χ₂) is nonnegative. At every natural number each quadratic value is 0, 1, or -1, and the coefficient is the product (1 + χ₁(n))(1 + χ₂(n)).

theorem AnalyticNumberTheory.LargeSieve.TatuzawaMultiplicativeTransfer.fourFactor_logDerivativeTerm_nonneg {q₁ q₂ : ℕ} (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) (h₁ : χ₁ ^ 2 = 1) (h₂ : χ₂ ^ 2 = 1) (σ : ℝ) (n : ℕ) : 0 ≤ (LSeries.term ((fun (n : ℕ) => 1 ↑n) * fun (n : ℕ) => ↑(ArithmeticFunction.vonMangoldt n)) (↑σ) n).re + (LSeries.term ((fun (n : ℕ) => χ₁ ↑n) * fun (n : ℕ) => ↑(ArithmeticFunction.vonMangoldt n)) (↑σ) n).re + (LSeries.term ((fun (n : ℕ) => χ₂ ↑n) * fun (n : ℕ) => ↑(ArithmeticFunction.vonMangoldt n)) (↑σ) n).re + (LSeries.term ((fun (n : ℕ) => (pairCharacter χ₁ χ₂) ↑n) * fun (n : ℕ) => ↑(ArithmeticFunction.vonMangoldt n)) (↑σ) n).re

Termwise von-Mangoldt positivity for the logarithmic derivative of the four-factor Euler product.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaMultiplicativeTransfer.fourFactor_negLogDerivative_nonneg {q₁ q₂ : ℕ} [NeZero q₁] [NeZero q₂] [NeZero (q₁ * q₂)] (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) (h₁ : χ₁ ^ 2 = 1) (h₂ : χ₂ ^ 2 = 1) (σ : ℝ) (hσ : 1 < σ) : 0 ≤ (-deriv (LSeries fun (x : ℕ) => 1) ↑σ / LSeries (fun (x : ℕ) => 1) ↑σ).re + (-deriv (LSeries fun (n : ℕ) => χ₁ ↑n) ↑σ / LSeries (fun (n : ℕ) => χ₁ ↑n) ↑σ).re + (-deriv (LSeries fun (n : ℕ) => χ₂ ↑n) ↑σ / LSeries (fun (n : ℕ) => χ₂ ↑n) ↑σ).re + (-deriv (LSeries fun (n : ℕ) => (pairCharacter χ₁ χ₂) ↑n) ↑σ / LSeries (fun (n : ℕ) => (pairCharacter χ₁ χ₂) ↑n) ↑σ).re

The negative logarithmic derivative of ζ(s)L(s,χ₁)L(s,χ₂)L(s,χ₁χ₂) is nonnegative on the real half-line σ > 1. This is the source-free Euler-product positivity bearing for the subsequent Deuring--Heilbronn zero-repulsion argument.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaMultiplicativeTransfer.integral_fourFactor_negLogDerivative_nonneg {q₁ q₂ : ℕ} [NeZero q₁] [NeZero q₂] [NeZero (q₁ * q₂)] (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) (h₁ : χ₁ ^ 2 = 1) (h₂ : χ₂ ^ 2 = 1) {a b : ℝ} (ha : 1 < a) (hab : a ≤ b) : 0 ≤ ∫ (σ : ℝ) in a..b, (-deriv (LSeries fun (x : ℕ) => 1) ↑σ / LSeries (fun (x : ℕ) => 1) ↑σ).re + (-deriv (LSeries fun (n : ℕ) => χ₁ ↑n) ↑σ / LSeries (fun (n : ℕ) => χ₁ ↑n) ↑σ).re + (-deriv (LSeries fun (n : ℕ) => χ₂ ↑n) ↑σ / LSeries (fun (n : ℕ) => χ₂ ↑n) ↑σ).re + (-deriv (LSeries fun (n : ℕ) => (pairCharacter χ₁ χ₂) ↑n) ↑σ / LSeries (fun (n : ℕ) => (pairCharacter χ₁ χ₂) ↑n) ↑σ).re

Integrated monotonicity of the four-factor negative logarithmic derivative on every compact real interval to the right of one. This is the exact calculus consequence of Euler-coefficient positivity: no zero-repulsion or value-product hypothesis is inserted.