Documentation

MathlibNt.AnalyticNumberTheory.Vaughan.VaughanDirectAPNormalizedTypeIIActualPhysical

Physical AP-normalized bounds for actual Vaughan Type-II shells #

This file starts with the genuine collected hyperbolic-prefix maximum. It applies prefix-maximal large sieve row by row, sums the rows after paying the Möbius energy, and only then uses Cauchy in primitive characters and moduli.

source
theorem AnalyticNumberTheory.LargeSieve.card_primitiveCharacter_le_totient (q : ℕ) (hq : 0 < q) :
Fintype.card (PrimitiveCharacter q) ≤ q.totient

Primitive characters form a subtype of all characters, whose cardinality is φ(q). This discharges the elementary cardinality side condition in direct Cauchy estimates.

source
theorem AnalyticNumberTheory.LargeSieve.apNormalizedVaughanActualCollectedShellMean_sq_le (N Q u v k l : ℕ) :
apNormalizedVaughanActualCollectedShellMean N Q u v k l ^ 2 ≤ conductorHarmonicFactor Q * ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, vaughanCanonicalCollectedPrefixMaxSquare N u v k l q χ

Double Cauchy for one actual collected shell. The first Cauchy is over primitive characters at fixed modulus; the second uses q⁻¹/², producing the exact q/φ(q) weight consumed by the prefix large sieve.

source
theorem AnalyticNumberTheory.LargeSieve.apNormalizedVaughanActualCollectedShellMean_sq_le_rowPrefixEnergy (N Q u v k l : ℕ) (hQ : 0 < Q) :
apNormalizedVaughanActualCollectedShellMean N Q u v k l ^ 2 ≤ conductorHarmonicFactor Q * (↑((vaughanCanonicalTensorLength N k).log2 + 1) ^ 2 * (↑N + ↑(2 ^ k) * ((2 * ↑⌈Real.log (↑Q ^ 2) / Real.log 2⌉₊ + 12) * ↑Q ^ 2)) * (27 * ↑N * Real.log ↑(N + 1) ^ 5))

Rowwise prefix-maximal large sieve, followed by Möbius energy and the unconditional divisor-square tensor-energy estimate.

source
theorem AnalyticNumberTheory.LargeSieve.pow_mul_cutoff_succ_le_two_mul_of_active {N u v k l : ℕ} (huv : u ≤ v) (hkl : (k, l) ∈ vaughanTypeIIActiveCanonicalRectangles N u v) :
2 ^ k * (u + 1) ≤ 2 * N

On an active rectangle, the lower d endpoint times u+1 is at most 2N, provided the second Vaughan cutoff is at least the first. The factor two is exactly the price of the cutoff-truncated dyadic e shell.

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

Explicit polylogarithmic payment for every actual Type-II shell.

Equations
Instances For
    source
    theorem AnalyticNumberTheory.LargeSieve.vaughanActualTypeIILogPay_nonneg (N Q : ℕ) :
    0 ≤ vaughanActualTypeIILogPay N Q
    source
    theorem AnalyticNumberTheory.LargeSieve.apNormalizedVaughanActualCollectedShellMean_physical (N Q u v k l : ℕ) (hQ : 0 < Q) (huv : u ≤ v) (hkl : (k, l) ∈ vaughanTypeIIActiveCanonicalRectangles N u v) :
    apNormalizedVaughanActualCollectedShellMean N Q u v k l ≤ vaughanActualTypeIILogPay N Q * (↑N + ↑Q * ↑N / √↑(u + 1))

    Physical bound for a genuine hyperbolic shell. Its proof uses the actual collected-prefix square, row-prefix maximal large sieve, Möbius energy, and only afterwards double Cauchy. No shell estimate occurs among the premises.

    source
    theorem AnalyticNumberTheory.LargeSieve.vaughanDirectAPNormalizedTypeIIInput_unconditional (N Q u v : ℕ) (hQ : 0 < Q) (huv : u ≤ v) :
    VaughanDirectAPNormalizedTypeIIInput N Q u v (↑(vaughanTypeIIActiveCanonicalRectangles N u v).card) (vaughanActualTypeIILogPay N Q)

    Unconditional analytic Type-II input: all shell estimates are produced in this module. The only parameter relation is the standard Vaughan choice u ≤ v; there is no per-shell premise.