Two-character induction with the missing Euler factors retained

This modern reduction uses a common multiple of the two levels, not a coprimality assumption. The product character need not be primitive. All three finite Euler products remain in the analytic identity.

theorem DirichletCharacter.instNeZeroNatConductorComplex_mathlibNt {Q : ℕ} (χ : DirichletCharacter ℂ Q) [NeZero Q] : NeZero χ.conductor

noncomputable def DirichletCharacter.inductionEulerProduct {q : ℕ} (χ : DirichletCharacter ℂ q) (Q : ℕ) (s : ℂ) : ℂ

The exact Euler correction when a character is induced to level Q.

Equations

• χ.inductionEulerProduct Q s = ∏ p ∈ Q.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

theorem DirichletCharacter.sq_changeLevel_eq_one {q Q : ℕ} (h : q ∣ Q) {χ : DirichletCharacter ℂ q} (hχ : χ ^ 2 = 1) : (changeLevel h) χ ^ 2 = 1

theorem DirichletCharacter.sq_mul_eq_one {Q : ℕ} {χ ψ : DirichletCharacter ℂ Q} (hχ : χ ^ 2 = 1) (hψ : ψ ^ 2 = 1) : (χ * ψ) ^ 2 = 1

theorem DirichletCharacter.mul_ne_one_of_quadratic_ne {Q : ℕ} {χ ψ : DirichletCharacter ℂ Q} (hψ : ψ ^ 2 = 1) (hne : χ ≠ ψ) : χ * ψ ≠ 1

Distinct quadratic characters have nonprincipal product.

theorem DirichletCharacter.changeLevel_ne_of_primitive_values {q r Q : ℕ} [NeZero Q] (hq : q ∣ Q) (hr : r ∣ Q) (χ : DirichletCharacter ℂ q) (ψ : DirichletCharacter ℂ r) (hχ : χ.IsPrimitive) (hψ : ψ.IsPrimitive) (hne : ∃ (n : ℕ), χ ↑n ≠ ψ ↑n) : (changeLevel hq) χ ≠ (changeLevel hr) ψ

Distinct primitive characters remain distinct at any common multiple. Distinctness is stated by their actual values, even when the levels differ.

theorem DirichletCharacter.primitiveCharacter_sq_eq_one {Q : ℕ} [NeZero Q] {χ : DirichletCharacter ℂ Q} (hχ : χ ^ 2 = 1) : χ.primitiveCharacter ^ 2 = 1

theorem DirichletCharacter.primitiveCharacter_ne_one_of_ne_one {Q : ℕ} {χ : DirichletCharacter ℂ Q} (hχ : χ ≠ 1) : χ.primitiveCharacter ≠ 1

theorem DirichletCharacter.LFunction_eq_primitive_mul_inductionEulerProduct {Q : ℕ} [NeZero Q] (χ : DirichletCharacter ℂ Q) {s : ℂ} (hs : χ ≠ 1 ∨ s ≠ 1) : LFunction χ s = LFunction χ.primitiveCharacter s * χ.primitiveCharacter.inductionEulerProduct Q s

The conductor reduction is an equality for the actual continued L-function, including at one when the character is nonprincipal.

theorem DirichletCharacter.twoCharacter_LFunction_product_induction {q r Q : ℕ} [NeZero q] [NeZero r] [NeZero Q] (hq : q ∣ Q) (hr : r ∣ Q) (χ : DirichletCharacter ℂ q) (ψ : DirichletCharacter ℂ r) {s : ℂ} (hχ : χ ≠ 1 ∨ s ≠ 1) (hψ : ψ ≠ 1 ∨ s ≠ 1) (hprod : (changeLevel hq) χ * (changeLevel hr) ψ ≠ 1 ∨ s ≠ 1) : riemannZeta s * LFunction ((changeLevel hq) χ) s * LFunction ((changeLevel hr) ψ) s * LFunction ((changeLevel hq) χ * (changeLevel hr) ψ) s = riemannZeta s * LFunction χ s * LFunction ψ s * LFunction ((changeLevel hq) χ * (changeLevel hr) ψ).primitiveCharacter s * (χ.inductionEulerProduct Q s * ψ.inductionEulerProduct Q s * ((changeLevel hq) χ * (changeLevel hr) ψ).primitiveCharacter.inductionEulerProduct Q s)

Full induction identity for the actual four-factor product. Neither the levels nor the conductor of their product are assumed coprime.

theorem DirichletCharacter.norm_inductionEulerProduct_le {q : ℕ} (χ : DirichletCharacter ℂ q) (Q : ℕ) (β : ℝ) : ‖χ.inductionEulerProduct Q ↑β‖ ≤ ∏ p ∈ Q.primeFactors, (1 + ↑p ^ (-β))

Explicit upper Euler loss at every real argument.

theorem DirichletCharacter.prod_one_sub_rpow_le_norm_inductionEulerProduct {q : ℕ} (χ : DirichletCharacter ℂ q) (Q : ℕ) {β : ℝ} (hβ : 0 < β) : ∏ p ∈ Q.primeFactors, (1 - ↑p ^ (-β)) ≤ ‖χ.inductionEulerProduct Q ↑β‖

The full lower Euler loss is retained, rather than silently identifying an imprimitive L-value with its primitive L-value.

theorem DirichletCharacter.inductionEulerProduct_ne_zero {q : ℕ} (χ : DirichletCharacter ℂ q) (Q : ℕ) {β : ℝ} (hβ : 0 < β) : χ.inductionEulerProduct Q ↑β ≠ 0

Euler induction creates no positive-real zero, even for nonquadratic characters or overlapping levels.

theorem DirichletCharacter.LFunction_changeLevel_real_eq_zero_iff {q Q : ℕ} [NeZero q] [NeZero Q] (hq : q ∣ Q) (χ : DirichletCharacter ℂ q) {β : ℝ} (hβ : 0 < β) (hχ : χ ≠ 1 ∨ β ≠ 1) : LFunction ((changeLevel hq) χ) ↑β = 0 ↔ LFunction χ ↑β = 0

In particular, a produced real zero persists under induction and reflects back to the original character; the bad-prime factors cannot create it.

theorem DirichletCharacter.LFunction_real_eq_zero_iff_primitive {Q : ℕ} [NeZero Q] (χ : DirichletCharacter ℂ Q) {β : ℝ} (hβ : 0 < β) (hχ : χ ≠ 1 ∨ β ≠ 1) : LFunction χ ↑β = 0 ↔ LFunction χ.primitiveCharacter ↑β = 0

Exact primitive reduction of a positive-real zero of an imprimitive character, including a nonprincipal character at one.

noncomputable def DirichletCharacter.twoCharacterResidue {Q : ℕ} [NeZero Q] (χ ψ : DirichletCharacter ℂ Q) : ℂ

The actual residue coefficient, not an independently chosen main term.

Equations

• χ.twoCharacterResidue ψ = DirichletCharacter.LFunction χ 1 * DirichletCharacter.LFunction ψ 1 * DirichletCharacter.LFunction (χ * ψ) 1

theorem DirichletCharacter.twoCharacter_product_residue_one {Q : ℕ} [NeZero Q] (χ ψ : DirichletCharacter ℂ Q) (hχ : χ ≠ 1) (hψ : ψ ≠ 1) (hprod : χ * ψ ≠ 1) : Filter.Tendsto (fun (s : ℂ) => (s - 1) * (riemannZeta s * LFunction χ s * LFunction ψ s * LFunction (χ * ψ) s)) (nhdsWithin 1 {1}ᶜ) (nhds (χ.twoCharacterResidue ψ))

The four-factor function has this actual residue at one whenever all three character factors are nonprincipal.

theorem DirichletCharacter.twoCharacterResidue_pos {Q : ℕ} [NeZero Q] {χ ψ : DirichletCharacter ℂ Q} (hχ : χ ^ 2 = 1) (hψ : ψ ^ 2 = 1) (hχ1 : χ ≠ 1) (hψ1 : ψ ≠ 1) (hne : χ ≠ ψ) : 0 < χ.twoCharacterResidue ψ

Distinct nonprincipal quadratic characters give a strictly positive real residue. Distinctness is essential: the diagonal has another pole.

theorem DirichletCharacter.twoCharacterResidue_induction {q r Q : ℕ} [NeZero q] [NeZero r] [NeZero Q] (hq : q ∣ Q) (hr : r ∣ Q) (χ : DirichletCharacter ℂ q) (ψ : DirichletCharacter ℂ r) (hχ : χ ≠ 1) (hψ : ψ ≠ 1) (hprod : (changeLevel hq) χ * (changeLevel hr) ψ ≠ 1) : ((changeLevel hq) χ).twoCharacterResidue ((changeLevel hr) ψ) = LFunction χ 1 * LFunction ψ 1 * LFunction ((changeLevel hq) χ * (changeLevel hr) ψ).primitiveCharacter 1 * (χ.inductionEulerProduct Q 1 * ψ.inductionEulerProduct Q 1 * ((changeLevel hq) χ * (changeLevel hr) ψ).primitiveCharacter.inductionEulerProduct Q 1)

The main-term coefficient after arbitrary common-level induction, with all three missing Euler products explicit.