Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.StandardBVPayload

Closed elementary payload for Standard Bombieri--Vinogradov #

This module packages the elementary lanes left by the low/high conductor split. The asymptotic payment is proved from Mathlib's Real.isLittleO_pow_log_id_atTop; no scalar asymptotic inequality is retained as a premise.

source
theorem AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMeanOn_vaughanSmall_le_explicit (N v : ℕ) (S : Finset ℕ) (hS : ∀ q ∈ S, 0 < q) :
apNormalizedPrimitiveMeanOn (vaughanSmallCoeff vaughanUnitIntegerCoeff v) N S ≤ ↑S.card * (↑v * Real.log ↑(v + 1))

The small Vaughan lane in AP normalization costs only the number of conductors, rather than a large-sieve square mean.

Inspect dependencies

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

source
theorem AnalyticNumberTheory.LargeSieve.highConductorVaughanSmallMean_le_explicit (N Q C v : ℕ) :
highConductorVaughanSmallMean N Q C v ≤ ↑Q * (↑v * Real.log ↑(v + 1))

In particular a conductor interval contained in [1,Q] costs at most Q v log(v+1).

Inspect dependencies

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

source
noncomputable def AnalyticNumberTheory.LargeSieve.StandardBVPayload (N Q : ℕ) :
ℝ

A convenient closed packet for exactly the elementary Standard-BV lanes.

Equations
Instances For
    Inspect dependencies

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

    source
    theorem AnalyticNumberTheory.LargeSieve.natLog2_cast_le_two_log {n : ℕ} (hn : 2 ≤ n) :
    ↑n.log2 ≤ 2 * Real.log ↑n
    Inspect dependencies

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

    source
    theorem AnalyticNumberTheory.LargeSieve.natSqrt_cast_le_realSqrt (n : ℕ) :
    ↑n.sqrt ≤ √↑n
    Inspect dependencies

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

    source
    theorem AnalyticNumberTheory.LargeSieve.Q_sqrt_log_payable (A k : ℕ) :
    ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (Q : ℕ), ↑Q ≤ √↑N / Real.log ↑N ^ (A + k) → ↑Q * (√↑N + 1) * Real.log ↑N ^ k ≤ 2 * ↑N / Real.log ↑N ^ A

    The exact Q ≤ sqrt N / log^(A+k) N calculation. This is the reusable polynomial-versus-log payment lemma for every elementary lane below.

    Inspect dependencies

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

    source
    theorem AnalyticNumberTheory.LargeSieve.StandardBVPayload_le_explicit :
    ∀ᶠ (N : ℕ) in Filter.atTop, ∀ Q ≤ N, StandardBVPayload N Q ≤ 90 * ↑Q * (√↑N + 1) * Real.log ↑N ^ 3

    Abel, bad-principal, higher-prime-power, and conductor-change terms have a single explicit Q (sqrt N+1) log^3 N envelope throughout the BV-relevant range Q ≤ N.

    Inspect dependencies

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

    source
    theorem AnalyticNumberTheory.LargeSieve.StandardBVPayload_payable (A : ℕ) :
    ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (Q : ℕ), ↑Q ≤ √↑N / Real.log ↑N ^ (A + 3) → StandardBVPayload N Q ≤ 180 * ↑N / Real.log ↑N ^ A

    For every requested logarithmic saving, choosing the modulus exponent three larger pays the entire closed elementary packet.

    Inspect dependencies

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