AP-normalized direct Vaughan assembly

This module is the direct L¹ route with the literal arithmetic-progression weight 1 / φ(q). The historical q / φ(q) unsquared mean remains available only as a compatibility majorant in VaughanDirectL1Physical.

noncomputable def AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIIMean (N Q u v : ℕ) : ℝ

AP-normalized Type-II direct Vaughan mean.

Equations

• AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIIMean N Q u v = AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMean (AnalyticNumberTheory.LargeSieve.vaughanTypeIICoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff u v) N Q

noncomputable def AnalyticNumberTheory.LargeSieve.apNormalizedVaughanSmallMean (N Q v : ℕ) : ℝ

AP-normalized small-range direct Vaughan mean.

Equations

• AnalyticNumberTheory.LargeSieve.apNormalizedVaughanSmallMean N Q v = AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMean (AnalyticNumberTheory.LargeSieve.vaughanSmallCoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff v) N Q

theorem AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMean_nonneg (a : ℤ → ℂ) (N Q : ℕ) : 0 ≤ apNormalizedPrimitiveMean a N Q

theorem AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMean_sq_le_harmonic_weightedSquare (a : ℤ → ℂ) (N Q : ℕ) (hcard : ∀ q ∈ Finset.Icc 1 Q, Fintype.card (PrimitiveCharacter q) ≤ q.totient) : apNormalizedPrimitiveMean a N Q ^ 2 ≤ conductorHarmonicFactor Q * ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare a 0 N q χ

Weighted Cauchy in the modulus variable. The reciprocal square roots produce the harmonic factor, while the second factor is exactly the usual q / φ(q) square-large-sieve ledger. Thus q / φ(q) appears only inside the proved square estimate, never as the direct unsquared mean.

theorem AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMean_vaughan_le (N Q u v : ℕ) : apNormalizedPrimitiveMean vonMangoldtIntegerCoeff N Q ≤ 2 * (apNormalizedVaughanTypeIMean N Q u v + apNormalizedVaughanTypeIIMean N Q u v + apNormalizedVaughanSmallMean N Q v)

Vaughan's exact three-piece identity assembled directly in the AP-normalized primitive L¹ mean.

theorem AnalyticNumberTheory.LargeSieve.direct_conductor_sum_le_apNormalizedPrimitive (a : ℤ → ℂ) (N Q : ℕ) : ∑ d ∈ Finset.Icc 2 Q, directConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, primitivePrefixAmplitude a N d ψ ≤ conductorHarmonicFactor Q ^ 2 * apNormalizedPrimitiveMean a N Q

Strong conductor transport. The exact reciprocal-totient conductor bound lands on the AP-normalized primitive mean, with no q / φ(q) inflation.

theorem AnalyticNumberTheory.LargeSieve.directAllCharacterMean_le_apNormalizedPrimitive (a : ℤ → ℂ) (N Q : ℕ) : directAllCharacterMean a N Q ≤ 2 * conductorHarmonicFactor Q ^ 2 * apNormalizedPrimitiveMean a N Q + 2 * directConductorCorrectionMean a N Q

All nonprincipal characters transported to the AP-normalized primitive mean. The change-of-level correction remains explicit.

def AnalyticNumberTheory.LargeSieve.vaughanTypeIShortScale (u v : ℕ) : ℕ

Largest short-variable scale occurring in the two Type-I lanes.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIShortScale u v = max u (u * v)

def AnalyticNumberTheory.LargeSieve.VaughanDirectAPNormalizedTypeIInput (N Q u v : ℕ) (K logPay : ℝ) : Prop

AP-normalized Type-I physical-scale input, retaining the exact Q*sqrt(N*D) dependence of the shell square ledger.

Equations

• AnalyticNumberTheory.LargeSieve.VaughanDirectAPNormalizedTypeIInput N Q u v K logPay = (AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIMean N Q u v ≤ K * logPay * (↑N + ↑Q ^ 2 * √↑N))

def AnalyticNumberTheory.LargeSieve.VaughanDirectAPNormalizedTypeIIInput (N Q u v : ℕ) (K logPay : ℝ) : Prop

AP-normalized Type-II physical-scale input.

Equations

• AnalyticNumberTheory.LargeSieve.VaughanDirectAPNormalizedTypeIIInput N Q u v K logPay = (AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIIMean N Q u v ≤ K * logPay * (↑N + ↑Q * ↑N / √↑(u + 1)))

theorem AnalyticNumberTheory.LargeSieve.direct_L1_vaughan_apNormalized_physical_assembly (E : ℕ → ℝ) (N Q u v : ℕ) (K logPay : ℝ) (hK : 0 ≤ K) (hlogPay : 0 ≤ logPay) (hE : ∀ q ∈ Finset.Icc 1 Q, E q ≤ (↑q.totient)⁻¹ * ∑ χ ∈ nonprincipalCharacters q, nonprincipalPrefixAmplitude vonMangoldtIntegerCoeff N q χ) (hI : VaughanDirectAPNormalizedTypeIInput N Q u v K logPay) (hII : VaughanDirectAPNormalizedTypeIIInput N Q u v K logPay) : ∑ q ∈ Finset.Icc 1 Q, E q ≤ 4 * conductorHarmonicFactor Q ^ 2 * (2 * vaughanDirectPhysicalMajorant N Q u K logPay + apNormalizedVaughanSmallMean N Q v) + 2 * directConductorCorrectionMean vonMangoldtIntegerCoeff N Q

Physical direct assembly through the AP-normalized primitive mean. In particular, conductor transport never invokes the compatibility q / φ(q) unsquared mean.