Subpower upper bounds for the actual two-character residue

The target character's original L-value is retained. Its induction correction, and the other two L-values at the common modulus, cost only logarithms. No coprimality or primitivity is needed for these upper bounds.

theorem DirichletCharacter.norm_LFunction_one_le_log_add_three {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) : ‖LFunction χ 1‖ ≤ Real.log ↑q + 3

Harmonic truncation at the modulus gives a logarithmic bound even for imprimitive nonprincipal characters.

theorem DirichletCharacter.norm_inductionEulerProduct_one_le_one_add_log {q : ℕ} (χ : DirichletCharacter ℂ q) (Q : ℕ) [NeZero Q] : ‖χ.inductionEulerProduct Q 1‖ ≤ 1 + Real.log ↑Q

Inducing any character to a nonzero common modulus has logarithmic Euler loss at one, including overlapping levels.

theorem DirichletCharacter.log_add_three_le_subpower {a x : ℝ} (ha : 0 < a) (hx : 1 ≤ x) : Real.log x + 3 ≤ (3 + 1 / a) * x ^ a

An explicit subpower majorant valid on the entire interval [1, ∞).

theorem DirichletCharacter.norm_LFunction_one_le_subpower {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {a : ℝ} (ha : 0 < a) : ‖LFunction χ 1‖ ≤ (3 + 1 / a) * ↑q ^ a

Arbitrarily small positive powers bound all nonprincipal L-values uniformly in the modulus.

theorem DirichletCharacter.norm_inductionEulerProduct_one_le_subpower {q : ℕ} (χ : DirichletCharacter ℂ q) (Q : ℕ) [NeZero Q] {a : ℝ} (ha : 0 < a) : ‖χ.inductionEulerProduct Q 1‖ ≤ (3 + 1 / a) * ↑Q ^ a

The target's missing Euler factors also have arbitrarily small power cost.

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

For a quadratic nonprincipal character its norm is its positive real value.

theorem DirichletCharacter.twoCharacterResidue_re_le_original_value_mul_subpower {q Q : ℕ} [NeZero q] [NeZero Q] (hq : q ∣ Q) (χ : DirichletCharacter ℂ q) (ψ : DirichletCharacter ℂ Q) (hχ : χ ≠ 1) (hquad : χ ^ 2 = 1) (hψ : ψ ≠ 1) (hprod : (changeLevel hq) χ * ψ ≠ 1) {a : ℝ} (ha : 0 < a) : (((changeLevel hq) χ).twoCharacterResidue ψ).re ≤ (LFunction χ 1).re * ((3 + 1 / a) ^ 3 * ↑Q ^ (3 * a))

Only the target's L-value is pulled back to its original modulus. The correction remains explicit; the other two factors are bounded at Q.