Linear-polylogarithmic control of imprimitive conductor multiplicity

This independent strengthening replaces the quadratic fibre estimate by the average order of the divisor function. The proof is completely finite: n = ∑ d ∣ n, φ(d) bounds n / φ(n) by the number of divisors, the divisor sum is transposed, and the resulting harmonic sum is bounded by a telescoping logarithm.

noncomputable def AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor (R : ℕ) : ℝ

A finite harmonic factor, including exactly the terms 1, ..., R.

Equations

• AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor R = ∑ e ∈ Finset.Icc 1 R, (↑e)⁻¹

theorem AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor_nonneg (R : ℕ) : 0 ≤ conductorHarmonicFactor R

theorem AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor_le (R : ℕ) : conductorHarmonicFactor R ≤ 1 + Real.log ↑R

The elementary telescoping logarithm bound for the finite harmonic factor.

theorem AnalyticNumberTheory.LargeSieve.totientRatio_le_card_divisors (n : ℕ) (hn : 0 < n) : ↑n / ↑n.totient ≤ ↑n.divisors.card

Divisor-sum control of one totient ratio.

theorem AnalyticNumberTheory.LargeSieve.sum_dvd_indicator_Icc (R e : ℕ) (he : 0 < e) : (∑ r ∈ Finset.Icc 1 R, if e ∣ r then 1 else 0) = ↑(R / e)

For fixed positive e, count its multiples up to R.

theorem AnalyticNumberTheory.LargeSieve.sum_totientRatio_le_linear_harmonic (R : ℕ) : ∑ r ∈ Finset.Icc 1 R, ↑r / ↑r.totient ≤ ↑R * conductorHarmonicFactor R

The finite average order of r / φ(r), with an explicit harmonic factor.

theorem AnalyticNumberTheory.LargeSieve.sum_totientRatio_le_linear_log (R : ℕ) : ∑ r ∈ Finset.Icc 1 R, ↑r / ↑r.totient ≤ ↑R * (1 + Real.log ↑R)

Explicit linear-logarithmic average totient-ratio estimate.

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

Multiplication by a conductor separates at the cost of r / φ(r).

theorem AnalyticNumberTheory.LargeSieve.imprimitiveConductorWeight_le_linear_harmonic (Q d : ℕ) (hd : 0 < d) : imprimitiveConductorWeight Q d ≤ ↑d / ↑d.totient * ↑(Q / d) * conductorHarmonicFactor (Q / d)

Strong imprimitive conductor bound: linear, rather than quadratic, in Q/d.

theorem AnalyticNumberTheory.LargeSieve.imprimitive_conductor_window_le_weighted_primitive_linear (F : (d : ℕ) → PrimitiveCharacter d → ℝ) (hF : ∀ (d : ℕ) (ψ : PrimitiveCharacter d), 0 ≤ F d ψ) (Q C : ℕ) (hC : 0 < C) : ∑ d ∈ Finset.Icc C (2 * C), imprimitiveConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, F d ψ ≤ ↑(Q / C) * conductorHarmonicFactor (Q / C) * ∑ d ∈ Finset.Icc 1 (2 * C), ↑d / ↑d.totient * ∑ ψ : PrimitiveCharacter d, F d ψ

Linear-harmonic conductor transport for an arbitrary nonnegative family. The existing prefix theorem is a specialization of this finite inequality.

theorem AnalyticNumberTheory.LargeSieve.imprimitiveConductorWeight_le_linear_log (Q d : ℕ) (hd : 0 < d) : imprimitiveConductorWeight Q d ≤ ↑d / ↑d.totient * ↑(Q / d) * (1 + Real.log ↑(Q / d))

Logarithmic presentation of the strong imprimitive conductor bound.

theorem AnalyticNumberTheory.LargeSieve.imprimitive_conductor_window_prefix_le_linear (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) * conductorHarmonicFactor (Q / D) * ∑ d ∈ Finset.Icc 1 (2 * D), ↑d / ↑d.totient * ∑ ψ : PrimitiveCharacter d, primitiveCharacterPrefixMaxSquare b M N d ψ

Dyadic-window transport with only the linear-harmonic conductor loss.

theorem AnalyticNumberTheory.LargeSieve.imprimitive_conductor_window_prefix_large_sieve_linear (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) * conductorHarmonicFactor (Q / D) * (↑(N.log2 + 1) ^ 2 * primitiveLargeSieveConstant N (2 * D) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖b n‖ ^ 2)

The strong conductor transport connected to the existing primitive maximal LS.

theorem AnalyticNumberTheory.LargeSieve.dyadic_linear_multiplicity_mul_modulus_sq_le (Q D : ℕ) (hD : 0 < D) (hDQ : D ≤ Q) : ↑(Q / D) * conductorHarmonicFactor (Q / D) * ↑(2 * D) ^ 2 ≤ 4 * ↑Q ^ 2 * conductorHarmonicFactor Q

Scale audit for the quadratic modulus term on every dyadic window D ≤ Q. The linear conductor loss leaves Q D, hence at most Q², times one harmonic factor. Summing all dyadic windows costs only the number of windows.