Explicit control of imprimitive conductor multiplicity

The exact conductor ledger counts a primitive character of conductor d once for every multiple q = d r. This module rewrites that fibre literally and then bounds it using the supermultiplicativity of Euler's totient. The quadratic coarse bound in Q / d is deliberately elementary; the final dyadic theorem records how this multiplicity is paid against the d² term in the primitive large sieve.

theorem AnalyticNumberTheory.LargeSieve.imprimitiveConductorWeight_eq_sum_multiples (Q d : ℕ) (hd : 0 < d) : imprimitiveConductorWeight Q d = ∑ r ∈ Finset.Icc 1 (Q / d), ↑(d * r) / ↑(d * r).totient

Rewrite the levels divisible by d as q = d r, without discarding the exact q / φ(q) weight.

theorem AnalyticNumberTheory.LargeSieve.multiple_totient_ratio_le (d r : ℕ) (hd : 0 < d) (hr : 0 < r) : ↑(d * r) / ↑(d * r).totient ≤ ↑d / ↑d.totient * ↑r

A factor in the multiple fibre is bounded by the conductor weight times its multiplicity parameter.

theorem AnalyticNumberTheory.LargeSieve.imprimitiveConductorWeight_le_sq (Q d : ℕ) (hd : 0 < d) : imprimitiveConductorWeight Q d ≤ ↑(Q / d) ^ 2 * (↑d / ↑d.totient)

Elementary explicit conductor-fibre bound. It is weaker than the optimal logarithmic estimate but has the precise shape needed by a dyadic BV argument: the extra multiplicity is at most (Q/d)².

theorem AnalyticNumberTheory.LargeSieve.imprimitive_conductor_window_le_weighted_primitive (F : (d : ℕ) → PrimitiveCharacter d → ℝ) (hF : ∀ (d : ℕ) (ψ : PrimitiveCharacter d), 0 ≤ F d ψ) (Q D : ℕ) (hD : 0 < D) : ∑ d ∈ Finset.Icc D (2 * D), imprimitiveConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, F d ψ ≤ ↑(Q / D) ^ 2 * ∑ d ∈ Finset.Icc D (2 * D), ↑d / ↑d.totient * ∑ ψ : PrimitiveCharacter d, F d ψ

Dyadic conductor-window transport. On D ≤ d ≤ 2D, the coarse fibre multiplicity costs (Q/D)²; what remains is exactly the weight d/φ(d) used by the primitive prefix large sieve.

theorem AnalyticNumberTheory.LargeSieve.imprimitive_conductor_window_prefix_le (b : ℤ → ℂ) (M : ℤ) (N Q D : ℕ) (hD : 0 < D) : ∑ d ∈ Finset.Icc D (2 * D), imprimitiveConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, primitiveCharacterPrefixMaxSquare b M N d ψ ≤ ↑(Q / D) ^ 2 * ∑ d ∈ Finset.Icc 1 (2 * D), ↑d / ↑d.totient * ∑ ψ : PrimitiveCharacter d, primitiveCharacterPrefixMaxSquare b M N d ψ

Direct specialization to primitive prefix maxima. Combined with weighted_primitive_prefix_maximal at modulus cutoff 2D, this is the exact bridge from the imprimitive conductor ledger to the existing primitive LS. The conductor window sum on the right is a nonnegative subsum of the range 1 ≤ d ≤ 2D.

theorem AnalyticNumberTheory.LargeSieve.imprimitive_conductor_window_prefix_large_sieve (b : ℤ → ℂ) (M : ℤ) (N Q D : ℕ) (hD : 0 < D) : ∑ d ∈ Finset.Icc D (2 * D), imprimitiveConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, primitiveCharacterPrefixMaxSquare b M N d ψ ≤ ↑(Q / D) ^ 2 * (↑(N.log2 + 1) ^ 2 * primitiveLargeSieveConstant N (2 * D) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖b n‖ ^ 2)

Fully discharged dyadic-window estimate. The factor (Q/D)² multiplies the primitive LS constant at cutoff 2D; in particular its quadratic modulus term is (Q/D)² (2D)² ≤ 4Q², uniformly in the dyadic conductor range.

theorem AnalyticNumberTheory.LargeSieve.dyadic_multiplicity_mul_modulus_sq_le (Q D : ℕ) : ↑(Q / D) ^ 2 * ↑(2 * D) ^ 2 ≤ 4 * ↑Q ^ 2

The key dyadic payment identity behind the preceding theorem. Although the elementary conductor-fibre estimate loses (Q/D)², this loss cancels the quadratic modulus scale (2D)² of the primitive large sieve, leaving at most 4Q². Thus the coarse bound is a genuine BV bound on the high-conductor ranges where the N term is no larger than the modulus-square term.