theorem DirichletCharacter.FourFactorLogInduction_euler_one_le {q Q : ℕ} (χ : DirichletCharacter ℂ q) (hQ : 0 < Q) : ‖χ.inductionEulerProduct Q 1‖ ≤ 1 + Real.log ↑Q

The actual finite induction correction costs only one logarithm. No primitivity or divisibility hypothesis is needed for this stronger bound.

theorem DirichletCharacter.FourFactorLogInduction_LFunction_one_le {Q : ℕ} [NeZero Q] (χ : DirichletCharacter ℂ Q) (hχ : χ ≠ 1) : ‖LFunction χ 1‖ ≤ 32 * (1 + Real.log ↑Q)

The full-modulus third L-value, not its primitive replacement, pays one log.

theorem DirichletCharacter.FourFactorLogInduction_norm_LFunction_one_eq_re {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (hχ : χ ≠ 1) : ‖LFunction χ 1‖ = (LFunction χ 1).re

theorem DirichletCharacter.FourFactorLogInduction_changeLevel_one_le {q Q : ℕ} [NeZero q] [NeZero Q] (hq : q ∣ Q) (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (hχ : χ ≠ 1) : ‖LFunction ((changeLevel hq) χ) 1‖ ≤ (LFunction χ 1).re * (1 + Real.log ↑Q)

Literal induction formula at one plus the finite Euler bound.

theorem DirichletCharacter.FourFactorLogInduction_residue_norm_le {q r Q : ℕ} [NeZero q] [NeZero r] [NeZero Q] (hq : q ∣ Q) (hr : r ∣ Q) (χ : DirichletCharacter ℂ q) (ψ : DirichletCharacter ℂ r) (hχquad : χ ^ 2 = 1) (hψquad : ψ ^ 2 = 1) (hχ : χ ≠ 1) (hψ : ψ ≠ 1) (hprod : (changeLevel hq) χ * (changeLevel hr) ψ ≠ 1) : ‖((changeLevel hq) χ).twoCharacterResidue ((changeLevel hr) ψ)‖ ≤ 32 * (1 + Real.log ↑Q) ^ 3 * (LFunction χ 1).re * (LFunction ψ 1).re

Two genuine lifts pay two logs and their nonprincipal product pays one. The constant is exactly 32; there is no polynomial modulus loss.

noncomputable def AnalyticNumberTheory.LargeSieve.FourFactorLogInduction_residue (x y : PrimitiveQuadraticDatum) : ℂ

The residue of the actual four-factor function after lifting both original primitive characters to the product level.

Equations

• AnalyticNumberTheory.LargeSieve.FourFactorLogInduction_residue x y = ((DirichletCharacter.changeLevel ⋯) x.character).twoCharacterResidue ((DirichletCharacter.changeLevel ⋯) y.character)

theorem AnalyticNumberTheory.LargeSieve.FourFactorLogInduction_residue_pos_and_le (x y : PrimitiveQuadraticDatum) (hxy : x ≠ y) : 0 < FourFactorLogInduction_residue x y ∧ (FourFactorLogInduction_residue x y).re ≤ 32 * (1 + Real.log ↑(x.modulus * y.modulus)) ^ 3 * x.value * y.value

Distinct primitive data supply the nonprincipal product internally.

theorem AnalyticNumberTheory.LargeSieve.FourFactorLogInduction_residue_re_pos_and_le (x y : PrimitiveQuadraticDatum) (hxy : x ≠ y) : 0 < (FourFactorLogInduction_residue x y).re ∧ (FourFactorLogInduction_residue x y).im = 0 ∧ (FourFactorLogInduction_residue x y).re ≤ 32 * (1 + Real.log ↑(x.modulus * y.modulus)) ^ 3 * x.value * y.value

Real-valued consumer form of the actual residue estimate.