Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.DirectConductorWeight

Direct reciprocal-totient conductor multiplicity #

This module proves the finite arithmetic estimate needed by the direct L¹ conductor regrouping. It is independent of the Vaughan decomposition.

source
noncomputable def AnalyticNumberTheory.LargeSieve.directConductorWeight (Q d : ℕ) :
ℝ

The exact conductor multiplicity for a direct 1 / φ(q) character sum.

Equations
Instances For
    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.directConductorWeight · compiled type and proof/definition references.

    source
    theorem AnalyticNumberTheory.LargeSieve.directConductorWeight_eq_sum_multiples (Q d : ℕ) (hd : 0 < d) :
    directConductorWeight Q d = ∑ r ∈ Finset.Icc 1 (Q / d), (↑(d * r).totient)⁻¹

    Rewrite the levels divisible by a positive d as q = d r.

    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.directConductorWeight_eq_sum_multiples · compiled type and proof/definition references.

    source
    theorem AnalyticNumberTheory.LargeSieve.multiple_inv_totient_le_product (d r : ℕ) (hd : 0 < d) (hr : 0 < r) :
    (↑(d * r).totient)⁻¹ ≤ (↑d.totient)⁻¹ * (↑r.totient)⁻¹

    Totient supermultiplicativity separates a reciprocal totient.

    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.multiple_inv_totient_le_product · compiled type and proof/definition references.

    source
    theorem AnalyticNumberTheory.LargeSieve.inv_totient_le_card_divisors_div (r : ℕ) (hr : 0 < r) :
    (↑r.totient)⁻¹ ≤ ↑r.divisors.card / ↑r

    The reciprocal totient is bounded by τ(r) / r.

    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.inv_totient_le_card_divisors_div · compiled type and proof/definition references.

    source
    theorem AnalyticNumberTheory.LargeSieve.sum_card_divisors_div_le_harmonic_sq (R : ℕ) :
    ∑ r ∈ Finset.Icc 1 R, ↑r.divisors.card / ↑r ≤ conductorHarmonicFactor R ^ 2

    The finite divisor-harmonic double sum is at most the square of the harmonic sum.

    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.sum_card_divisors_div_le_harmonic_sq · compiled type and proof/definition references.

    source
    theorem AnalyticNumberTheory.LargeSieve.sum_inv_totient_le_harmonic_sq (R : ℕ) :
    ∑ r ∈ Finset.Icc 1 R, (↑r.totient)⁻¹ ≤ conductorHarmonicFactor R ^ 2

    Finite average reciprocal-totient bound.

    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.sum_inv_totient_le_harmonic_sq · compiled type and proof/definition references.

    source
    theorem AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor_mono {R S : ℕ} (hRS : R ≤ S) :
    conductorHarmonicFactor R ≤ conductorHarmonicFactor S

    The harmonic factor is monotone in its natural cutoff.

    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor_mono · compiled type and proof/definition references.

    source
    theorem AnalyticNumberTheory.LargeSieve.directConductorWeight_le (Q d : ℕ) :
    directConductorWeight Q d ≤ conductorHarmonicFactor Q ^ 2 / ↑d.totient

    Strong unconditional direct conductor-weight bound, including d = 0, d > Q, and hence all empty-fibre cases. Unlike the compatibility majorant below, the primitive weight is exactly 1 / φ(d): no factor d is inserted.

    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.directConductorWeight_le · compiled type and proof/definition references.

    source
    theorem AnalyticNumberTheory.LargeSieve.directConductorWeight_le_compatibility_majorant (Q d : ℕ) :
    directConductorWeight Q d ≤ conductorHarmonicFactor Q ^ 2 * (↑d / ↑d.totient)

    Compatibility-only weakening to the historical square-large-sieve weight d / φ(d). New direct L¹ assembly should use directConductorWeight_le and the AP-normalized primitive mean instead.

    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.directConductorWeight_le_compatibility_majorant · compiled type and proof/definition references.