Direct Vaughan Type-I: the AP-normalized physical scale

The unsquared mean arising from character orthogonality has weight 1 / φ(q). This module keeps that weight through row Cauchy and only then invokes the existing variable-length primitive maximal large sieve. It also records why putting the square-large-sieve weight q / φ(q) on the unsquared mean inserts an extra factor q before any analytic estimate is used.

noncomputable def AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMean (a : ℤ → ℂ) (N Q : ℕ) : ℝ

The primitive unsquared mean with the weight produced by AP character orthogonality. This is deliberately distinct from the square-large-sieve weight q / φ(q).

Equations

• AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMean a N Q = ∑ q ∈ Finset.Icc 1 Q, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, AnalyticNumberTheory.LargeSieve.primitivePrefixAmplitude a N q χ

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

The corrected direct Type-I mean. The Vaughan input itself is not frozen: this is the literal producer quantity.

Equations

• AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIMean N Q u v = AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMean (AnalyticNumberTheory.LargeSieve.vaughanTypeICoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff u v) N Q

theorem AnalyticNumberTheory.LargeSieve.directPrimitiveMean_summand_eq_q_mul (a : ℤ → ℂ) (N q : ℕ) (_hq : 0 < q) : ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitivePrefixAmplitude a N q χ = ↑q * ((↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, primitivePrefixAmplitude a N q χ)

The old unsquared weight is exactly q times the AP-normalized summand.

theorem AnalyticNumberTheory.LargeSieve.directPrimitiveMean_summand_strictly_inflates (a : ℤ → ℂ) (N q : ℕ) (hq : 1 < q) (hA : 0 < ∑ χ : PrimitiveCharacter q, primitivePrefixAmplitude a N q χ) : (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, primitivePrefixAmplitude a N q χ < ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitivePrefixAmplitude a N q χ

Strict one-level scale counterexample: as soon as the primitive amplitude mass is positive and q>1, replacing 1/φ(q) by q/φ(q) strictly enlarges that level. Thus q/φ(q) cannot be called the direct AP-normalized L¹ mean; it is the square-large-sieve weight.

noncomputable def AnalyticNumberTheory.LargeSieve.apNormalizedVariableLengthRowMean {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (c : ι → ℤ → ℂ) (L : ι → ℕ) (Q : ℕ) : ℝ

Rowwise AP-normalized L¹ majorant. For Vaughan's first lane, S is a d-shell; for the middle lane it is a (d,e) shell.

Equations

• AnalyticNumberTheory.LargeSieve.apNormalizedVariableLengthRowMean S c L Q = ∑ q ∈ Finset.Icc 1 Q, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ∑ r ∈ S, √(AnalyticNumberTheory.LargeSieve.primitiveCharacterPrefixMaxSquare (c r) 0 (L r) q χ)

theorem AnalyticNumberTheory.LargeSieve.apNormalizedVariableLengthRowMean_sq_le {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (c : ι → ℤ → ℂ) (L : ι → ℕ) (Q : ℕ) (hcard : ∀ q ∈ Finset.Icc 1 Q, Fintype.card (PrimitiveCharacter q) ≤ q.totient) : apNormalizedVariableLengthRowMean S c L Q ^ 2 ≤ ↑(Finset.Icc 1 Q).card * ↑S.card * ∑ q ∈ Finset.Icc 1 Q, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ∑ r ∈ S, primitiveCharacterPrefixMaxSquare (c r) 0 (L r) q χ

Cauchy with the correct normalization. The exact number of rows and moduli is visible; no analytic hypothesis is hidden here.

theorem AnalyticNumberTheory.LargeSieve.apNormalized_variableLength_square_le_budget {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (c : ι → ℤ → ℂ) (L : ι → ℕ) (Q : ℕ) (hQ : 0 < Q) : ∑ q ∈ Finset.Icc 1 Q, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ∑ r ∈ S, primitiveCharacterPrefixMaxSquare (c r) 0 (L r) q χ ≤ variableLengthPrimitivePrefixBudget S c L Q

The AP-normalized square ledger is bounded by the existing variable-length large sieve. This is the precise point where the proved LS theorem is called.

theorem AnalyticNumberTheory.LargeSieve.apNormalizedVariableLengthRowMean_sq_le_budget {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (c : ι → ℤ → ℂ) (L : ι → ℕ) (Q : ℕ) (hQ : 0 < Q) (hcard : ∀ q ∈ Finset.Icc 1 Q, Fintype.card (PrimitiveCharacter q) ≤ q.totient) : apNormalizedVariableLengthRowMean S c L Q ^ 2 ≤ ↑(Finset.Icc 1 Q).card * ↑S.card * variableLengthPrimitivePrefixBudget S c L Q

Combined corrected-weight Cauchy + variable-length LS producer.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleShortEnergy_explicitLambda (DS ES : Finset ℕ) : vaughanTypeIMiddleShortEnergy DS ES ≤ ↑DS.card * ∑ e ∈ ES, ‖↑(ArithmeticFunction.vonMangoldt e)‖ ^ 2

The middle μ*Λ lane retains the literal Λ square energy; it is not silently replaced by a row count.

theorem AnalyticNumberTheory.LargeSieve.corrected_typeI_shell_physical_of_square (shellMean logPay N Q : ℝ) (hmean : 0 ≤ shellMean) (hlog : 0 ≤ logPay) (hN : 0 ≤ N) (_hQ : 0 ≤ Q) (hsq : shellMean ^ 2 ≤ (logPay * (N + Q ^ 2 * √N)) ^ 2) : shellMean ≤ logPay * (N + Q ^ 2 * √N)

Scalar shell optimization. If a corrected-weight shell has a square bound P², then it has the physical unsquared bound P; choosing P = logPay * (N + Q² sqrt N) is the exact producer shape.