Actual high-conductor Type-II shell-sum ledger

This module partitions the literal collected outer rows 1 ≤ r < 2^K into canonical shells. It retains the conductor window R < d ≤ Q and the actual short length N / 2^k separately for every shell. No full Type-II saving premise is used.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIICollectedPrefix (N K y d : ℕ) (a : ℕ → ℂ) (c : ℕ → ℕ → ℂ) (χ : PrimitiveCharacter d) : ℂ

The complete collected Type-II prefix before the canonical outer-shell partition.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIICollectedPrefix N K y d a c χ = ∑ k ∈ Finset.range K, ∑ r ∈ AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShell k, a r * ∑ t ∈ Finset.Icc 1 (min ↑y ↑(AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShellLength N k)), AnalyticNumberTheory.LargeSieve.vaughanTypeIICollectedRowCoefficient N r c t * ↑χ ↑t

theorem AnalyticNumberTheory.LargeSieve.sum_Ico_one_pow_two_eq_sum_vaughanTypeIIFixedShells (K : ℕ) (f : ℕ → ℂ) : ∑ r ∈ Finset.Ico 1 (2 ^ K), f r = ∑ k ∈ Finset.range K, ∑ r ∈ vaughanTypeIIFixedShell k, f r

Canonical powers-of-two shells partition the literal positive outer range.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIICollectedPrefix_eq_shellSum (N K y d : ℕ) (a : ℕ → ℂ) (c : ℕ → ℕ → ℂ) (χ : PrimitiveCharacter d) : vaughanTypeIICollectedPrefix N K y d a c χ = ∑ k ∈ Finset.range K, ∑ r ∈ vaughanTypeIIFixedShell k, a r * ∑ t ∈ Finset.Icc 1 (min ↑y ↑(vaughanTypeIIFixedShellLength N k)), vaughanTypeIICollectedRowCoefficient N r c t * ↑χ ↑t

The existing collected-row expression decomposes exactly into its canonical shell expressions; this is an identity, not a decomposition premise.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIICollectedPrefixSquare (N K y d : ℕ) (a : ℕ → ℂ) (c : ℕ → ℕ → ℂ) (χ : PrimitiveCharacter d) : ℝ

Literal complete-prefix square of the collected outer range.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIICollectedPrefixSquare N K y d a c χ = ‖AnalyticNumberTheory.LargeSieve.vaughanTypeIICollectedPrefix N K y d a c χ‖ ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIICollectedPrefixMaxSquare (N K d : ℕ) (a : ℕ → ℂ) (c : ℕ → ℕ → ℂ) (χ : PrimitiveCharacter d) : ℝ

Maximum over the same physical prefixes used by every fixed-shell row.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIICollectedPrefixMaxSquare N K d a c χ = (Finset.image (fun (y : ℕ) => AnalyticNumberTheory.LargeSieve.vaughanTypeIICollectedPrefixSquare N K y d a c χ) (Finset.range (N + 1))).max' ⋯

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIIShellSumMajorantSquare (N K d : ℕ) (a : ℕ → ℂ) (c : ℕ → ℕ → ℂ) (χ : PrimitiveCharacter d) : ℝ

Shell-sum square majorant. Every summand retains its own physical length N / 2^k through vaughanTypeIIFixedShellPrefixMaxSquare.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIIShellSumMajorantSquare N K d a c χ = ↑K * ∑ k ∈ Finset.range K, AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShellPrefixMaxSquare N k d a c χ

noncomputable def AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIIShellSumAmplitude (N K d : ℕ) (a : ℕ → ℂ) (c : ℕ → ℕ → ℂ) (χ : PrimitiveCharacter d) : ℝ

AP-normalized amplitude attached to the honest shell-sum majorant.

Equations

• AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIIShellSumAmplitude N K d a c χ = √(AnalyticNumberTheory.LargeSieve.vaughanTypeIIShellSumMajorantSquare N K d a c χ)

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIIShellSumMajorantSquare_nonneg (N K d : ℕ) (a : ℕ → ℂ) (c : ℕ → ℕ → ℂ) (χ : PrimitiveCharacter d) : 0 ≤ vaughanTypeIIShellSumMajorantSquare N K d a c χ

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIICollectedPrefixSquare_le_shellSumMajorant (N K y d : ℕ) (_hy : y ≤ N) (a : ℕ → ℂ) (c : ℕ → ℕ → ℂ) (χ : PrimitiveCharacter d) : vaughanTypeIICollectedPrefixSquare N K y d a c χ ≤ vaughanTypeIIShellSumMajorantSquare N K d a c χ

The exact collected-shell decomposition, followed only by finite shell Cauchy, bounds every physical prefix by the shell-sum majorant.

theorem AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIIShellSum_squareLedger_le (R Q N K : ℕ) (hQ : 0 < Q) (a : ℕ → ℂ) (c : ℕ → ℕ → ℂ) : (highConductorPrimitiveSquareLedger R Q fun (d : ℕ) => highConductorVaughanTypeIIShellSumAmplitude N K d a c) ≤ ↑K * ∑ k ∈ Finset.range K, ↑((vaughanTypeIIFixedShellLength N k).log2 + 1) ^ 2 * primitiveLargeSieveConstant (vaughanTypeIIFixedShellLength N k) Q * (vaughanTypeIIFixedShellOuterEnergy k a * vaughanTypeIIFixedShellTensorEnergy N k c)

High-conductor Type-II shell-sum square ledger. The conductor block R < d ≤ Q remains literal on the left. On the right each shell keeps its own length N / 2^k; no complete-saving premise occurs.

theorem AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIIShellSum_mean_sq_le (R Q N K : ℕ) (hQ : 0 < Q) (a : ℕ → ℂ) (c : ℕ → ℕ → ℂ) : (highConductorPrimitiveMean R Q fun (d : ℕ) => highConductorVaughanTypeIIShellSumAmplitude N K d a c) ^ 2 ≤ highConductorHarmonicTail R Q * (↑K * ∑ k ∈ Finset.range K, ↑((vaughanTypeIIFixedShellLength N k).log2 + 1) ^ 2 * primitiveLargeSieveConstant (vaughanTypeIIFixedShellLength N k) Q * (vaughanTypeIIFixedShellOuterEnergy k a * vaughanTypeIIFixedShellTensorEnergy N k c))

The genuine conductor Cauchy connector converts the shell-sum square ledger into the AP-normalized mean-square statement while retaining R through the harmonic tail.

Connector to the production hyperbolic collected-shell decomposition

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

The shell sum occurring on the right of the production exact hyperbolic-prefix decomposition. Unlike vaughanTypeIICollectedPrefix, this uses the actual canonical rectangle family and the actual collected-prefix maxima from VaughanDirectAPNormalizedTypeIIActualDecomposition.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIIProductionActualCollectedShellSum N Q u v = ∑ kl ∈ AnalyticNumberTheory.LargeSieve.vaughanTypeIIActiveCanonicalRectangles N u v, AnalyticNumberTheory.LargeSieve.apNormalizedVaughanActualCollectedShellMean N Q u v kl.1 kl.2

theorem AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIIMean_le_productionActualCollectedShellSum (N Q u v : ℕ) : apNormalizedVaughanTypeIIMean N Q u v ≤ vaughanTypeIIProductionActualCollectedShellSum N Q u v

The production direct Type-II mean is connected to the actual collected shell sum by the already-proved exact hyperbolic decomposition, rather than by a conclusion-shaped decomposition premise.