AP-normalized Vaughan Type-I shell input

This file isolates the weighted Cauchy step needed by the physical Type-I argument. In particular, Cauchy in the modulus variable is weighted by q^{-1/2}. The resulting first factor is the harmonic conductor ledger, not the cardinality of the modulus interval. Every row on the square side keeps its own length, so this module never forms a length-N global coefficient moment.

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

An AP-normalized shell of long rows with their literal short coefficients.

Equations

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

noncomputable def AnalyticNumberTheory.LargeSieve.rowShellShortEnergy {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (w : ι → ℂ) : ℝ

Literal square energy of the short coefficients in one shell.

Equations

• AnalyticNumberTheory.LargeSieve.rowShellShortEnergy S w = ∑ r ∈ S, ‖w r‖ ^ 2

theorem AnalyticNumberTheory.LargeSieve.apNormalizedWeightedRowShellMean_nonneg {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (w : ι → ℂ) (c : ι → ℤ → ℂ) (L : ι → ℕ) (Q : ℕ) : 0 ≤ apNormalizedWeightedRowShellMean S w c L Q

theorem AnalyticNumberTheory.LargeSieve.rowShellShortEnergy_nonneg {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (w : ι → ℂ) : 0 ≤ rowShellShortEnergy S w

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

Weighted Cauchy, first over primitive characters and then over the rows, with the correct q^{-1/2} outer weight. The square ledger on the right has exactly the q / φ(q) weight consumed by the primitive large sieve.

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

The previous shell square estimate with the variable-length primitive maximal large sieve inserted. This is the no-global-moment producer.

The two literal Vaughan Type-I lanes

noncomputable def AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIFirstShellMean (DS : Finset ℕ) (N Q : ℕ) : ℝ

One d-shell in the first (μ * log) lane. Its row has the physical length N / d; no coefficient is collected back at ambient length N.

Equations

• AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIFirstShellMean DS N Q = AnalyticNumberTheory.LargeSieve.apNormalizedWeightedRowShellMean DS (fun (d : ℕ) => ↑(ArithmeticFunction.moebius d)) (AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstRowCoeff fun (x : ℕ) => 1) (AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstRowLength N) Q

noncomputable def AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIMiddleShellMean (DS ES : Finset ℕ) (N Q : ℕ) : ℝ

One (d,e)-shell in the middle (μ * Λ) lane. Its row has the physical length N / (d*e).

Equations

• AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIMiddleShellMean DS ES N Q = AnalyticNumberTheory.LargeSieve.apNormalizedWeightedRowShellMean (DS ×ˢ ES) (fun (de : ℕ × ℕ) => ↑(ArithmeticFunction.moebius de.1) * ↑(ArithmeticFunction.vonMangoldt de.2)) (AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddlePairRowCoeff fun (x : ℕ) => 1) (AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddlePairRowLength N) Q

theorem AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIFirstShellMean_sq_le_budget (DS : Finset ℕ) (N Q : ℕ) (hQ : 0 < Q) (hcard : ∀ q ∈ Finset.Icc 1 Q, Fintype.card (PrimitiveCharacter q) ≤ q.totient) : apNormalizedVaughanTypeIFirstShellMean DS N Q ^ 2 ≤ conductorHarmonicFactor Q * vaughanTypeIFirstShortEnergy DS * variableLengthPrimitivePrefixBudget DS (vaughanTypeIFirstRowCoeff fun (x : ℕ) => 1) (vaughanTypeIFirstRowLength N) Q

theorem AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIMiddleShellMean_sq_le_budget (DS ES : Finset ℕ) (N Q : ℕ) (hQ : 0 < Q) (hcard : ∀ q ∈ Finset.Icc 1 Q, Fintype.card (PrimitiveCharacter q) ≤ q.totient) : apNormalizedVaughanTypeIMiddleShellMean DS ES N Q ^ 2 ≤ (conductorHarmonicFactor Q * rowShellShortEnergy (DS ×ˢ ES) fun (de : ℕ × ℕ) => ↑(ArithmeticFunction.moebius de.1) * ↑(ArithmeticFunction.vonMangoldt de.2)) * variableLengthPrimitivePrefixBudget (DS ×ˢ ES) (vaughanTypeIMiddlePairRowCoeff fun (x : ℕ) => 1) (vaughanTypeIMiddlePairRowLength N) Q

theorem AnalyticNumberTheory.LargeSieve.apNormalized_typeI_shell_physical (shellMean H E B D W R C N Q : ℝ) (hmean : 0 ≤ shellMean) (hH : 0 ≤ H) (_hE : 0 ≤ E) (hB : 0 ≤ B) (hD : 0 < D) (hW : 0 ≤ W) (hR : 0 ≤ R) (hC : 1 ≤ C) (hN : 0 ≤ N) (hQ : 0 ≤ Q) (hsq : shellMean ^ 2 ≤ H * E * B) (henergy : E ≤ D * W ^ 2) (hrow : D * B ≤ R ^ 2 * (N ^ 2 + C * Q ^ 2 * N * D)) : shellMean ≤ W * R * √(H * C) * (N + Q * √(N * D))

Scalar optimization used on each dyadic short-variable shell. Reopening the square ledger gives the exact short-scale term Q * sqrt (N*D). The older Q²*sqrt N is only what results after the lossy substitution D ≤ Q²; it is not intrinsic to double Cauchy.

theorem AnalyticNumberTheory.LargeSieve.vaughanDirectAPNormalizedTypeIInput_of_shells {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (firstShells : Finset α) (middleShells : Finset β) (firstMean : α → ℝ) (middleMean : β → ℝ) (N Q u v : ℕ) (logPay : ℝ) (_hlog : 0 ≤ logPay) (hdecomp : apNormalizedVaughanTypeIMean N Q u v ≤ ∑ s ∈ firstShells, firstMean s + ∑ s ∈ middleShells, middleMean s) (hfirst : ∀ s ∈ firstShells, firstMean s ≤ logPay * (↑N + ↑Q ^ 2 * √↑N)) (hmiddle : ∀ s ∈ middleShells, middleMean s ≤ logPay * (↑N + ↑Q ^ 2 * √↑N)) : VaughanDirectAPNormalizedTypeIInput N Q u v (↑(firstShells.card + middleShells.card)) logPay

Finite shell aggregation. This is the final wiring theorem used after the first lane (d shells) and middle lane ((d,e) shells) have separately been expanded. It records the explicit constant K = #first shells + #middle shells; the common logPay contains the RM, coefficient, harmonic, and large-sieve logarithmic payments supplied by the shell estimates.