Comparison against one fixed genuine real zero

The witness and its actual zero are chosen before the target character. Induction is to the product of the levels, without a coprimality assumption. The diagonal is handled by equality of the naturally ordered L-series.

theorem DirichletCharacter.LFunction_one_eq_of_nat_values_eq {q r : ℕ} [NeZero q] [NeZero r] (χ : DirichletCharacter ℂ q) (ψ : DirichletCharacter ℂ r) (hχ : χ ≠ 1) (hψ : ψ ≠ 1) (heq : ∀ (n : ℕ), χ ↑n = ψ ↑n) : LFunction χ 1 = LFunction ψ 1

Equality on the natural numbers identifies actual L-values, even when the two character levels are different.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.original_value_lower_bound_of_common_level_real_zero {q Q : ℕ} [NeZero q] [NeZero Q] (hq : q ∣ Q) (χ : DirichletCharacter ℂ q) (ψ : DirichletCharacter ℂ Q) (hχ : χ ≠ 1) (hψ : ψ ≠ 1) (hχquad : χ ^ 2 = 1) (hψquad : ψ ^ 2 = 1) (hne : (DirichletCharacter.changeLevel hq) χ ≠ ψ) {β a : ℝ} (hβ : 7 / 8 ≤ β) (hβ1 : β < 1) (hzero : DirichletCharacter.LFunction ψ ↑β = 0) (ha : 0 < a) : (1 - β) / (2 * 5000 ^ (8 * (1 - β)) * (3 + 1 / a) ^ 3) * ↑Q ^ (-(24 * (1 - β) + 3 * a)) ≤ (DirichletCharacter.LFunction χ 1).re

Combining the genuine residue lower bound with the subpower upper bound recovers the target's original L-value, retaining its induction loss.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.exists_fixed_witness_distinct_lower_bound {r : ℕ} [NeZero r] (ψ : DirichletCharacter ℂ r) (hψprim : ψ.IsPrimitive) (hψ : ψ ≠ 1) (hψquad : ψ ^ 2 = 1) {β a : ℝ} (hβ : 7 / 8 ≤ β) (hβ1 : β < 1) (hzero : DirichletCharacter.LFunction ψ ↑β = 0) (ha : 0 < a) : ∃ (c : ℝ), 0 < c ∧ ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), χ.IsPrimitive → χ ≠ 1 → χ ^ 2 = 1 → (∃ (n : ℕ), χ ↑n ≠ ψ ↑n) → c * ↑q ^ (-(24 * (1 - β) + 3 * a)) ≤ (DirichletCharacter.LFunction χ 1).re

One fixed primitive witness gives a uniform comparison for all distinct primitive targets; the fixed level is absorbed into the positive constant.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.exists_fixed_witness_lower_bound {r : ℕ} [NeZero r] (ψ : DirichletCharacter ℂ r) (hψprim : ψ.IsPrimitive) (hψ : ψ ≠ 1) (hψquad : ψ ^ 2 = 1) {β a : ℝ} (hβ : 7 / 8 ≤ β) (hβ1 : β < 1) (hzero : DirichletCharacter.LFunction ψ ↑β = 0) (ha : 0 < a) : ∃ (c : ℝ), 0 < c ∧ ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), χ.IsPrimitive → χ ≠ 1 → χ ^ 2 = 1 → c * ↑q ^ (-(24 * (1 - β) + 3 * a)) ≤ (DirichletCharacter.LFunction χ 1).re

The same witness bounds every target. Equality of the natural character values uses its actual positive L-value, not an enumeration of conductors.