Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.ImprimitiveConductorWeightLinear

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.

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

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

Equations
Instances For
    source
    theorem AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor_nonneg (R : ℕ) :
    0 ≤ conductorHarmonicFactor R
    source
    theorem AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor_le (R : ℕ) :
    conductorHarmonicFactor R ≤ 1 + Real.log ↑R

    The elementary telescoping logarithm bound for the finite harmonic factor.

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

    Divisor-sum control of one totient ratio.

    source
    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.

    source
    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.

    source
    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.

    source
    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).

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.