AP-normalized direct Type-II bilinear shells

The direct mean is formed before squaring. Cauchy is first taken over primitive characters and then over moduli with the outer weight q⁻¹/²; hence the square side has exactly the q / φ(q) weight accepted by the bilinear tensor large sieve. The canonical (d,t) tensor prefix remains intact throughout.

The resulting square scale on a d-shell is

H * RM² * D * (M + c(Q)Q²) * E(D,M).

For the actual tensor energy E(D,M) ≪ D M log⁵, taking the square root gives D M + sqrt(c(Q)) Q sqrt(D * D M), rather than another unsquared factor D M. Thus the existing second moment is sufficient for the direct shell. The final theorem below only aggregates already-physical shell bounds; it does not freeze a Type-II conclusion as a new analytic premise.

noncomputable def AnalyticNumberTheory.LargeSieve.apNormalizedVaughanCanonicalBilinearShellMean (b : ℕ → ℂ) (y N u v k l Q : ℕ) : ℝ

The unsquared AP-normalized mean of one actual canonical (d,t) tensor prefix. The maximum in t is inside each primitive-character summand.

Equations

• AnalyticNumberTheory.LargeSieve.apNormalizedVaughanCanonicalBilinearShellMean b y N u v k l Q = ∑ q ∈ Finset.Icc 1 Q, (↑q.totient)⁻¹ * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, √(AnalyticNumberTheory.LargeSieve.vaughanCanonicalBilinearPrefixMaxSquare b y N u v k l q χ)

theorem AnalyticNumberTheory.LargeSieve.apNormalizedVaughanCanonicalBilinearShellMean_nonneg (b : ℕ → ℂ) (y N u v k l Q : ℕ) : 0 ≤ apNormalizedVaughanCanonicalBilinearShellMean b y N u v k l Q

theorem AnalyticNumberTheory.LargeSieve.apNormalizedVaughanCanonicalBilinearShellMean_sq_le (b : ℕ → ℂ) (y N u v k l Q : ℕ) (hcard : ∀ q ∈ Finset.Icc 1 Q, Fintype.card (PrimitiveCharacter q) ≤ q.totient) : apNormalizedVaughanCanonicalBilinearShellMean b y N u v k l Q ^ 2 ≤ conductorHarmonicFactor Q * ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, vaughanCanonicalBilinearPrefixMaxSquare b y N u v k l q χ

The correct double Cauchy inequality for a direct bilinear shell. Character Cauchy is local to each modulus; modulus Cauchy uses q⁻¹/². Consequently no cardinality factor for the modulus interval and no second tensor energy appear.

theorem AnalyticNumberTheory.LargeSieve.apNormalizedVaughanCanonicalBilinearShellMean_sq_le_energy (b : ℕ → ℂ) (y N u v k l Q : ℕ) (hQ : 0 < Q) (hcard : ∀ q ∈ Finset.Icc 1 Q, Fintype.card (PrimitiveCharacter q) ≤ q.totient) : apNormalizedVaughanCanonicalBilinearShellMean b y N u v k l Q ^ 2 ≤ conductorHarmonicFactor Q * (↑((vaughanCanonicalTensorLength y k).log2 + 1) ^ 2 * ↑(2 ^ k) * (↑(vaughanCanonicalTensorLength y k) + primitiveBilinearQFactor Q * ↑Q ^ 2) * vaughanCanonicalShortTensorEnergy vaughanMangoldtCoeff b y N u v k l)

Existing bilinear tensor prefix large sieve inserted after the direct double Cauchy. The actual energy occurs exactly once.

theorem AnalyticNumberTheory.LargeSieve.apNormalizedVaughanCanonicalBilinearShellMean_sq_le_energy27 (b : ℕ → ℂ) (y N u v k l Q : ℕ) (B : ℝ) (hQ : 0 < Q) (hcard : ∀ q ∈ Finset.Icc 1 Q, Fintype.card (PrimitiveCharacter q) ≤ q.totient) (hB : ∀ n ≤ y, ‖b n‖ ≤ B) : apNormalizedVaughanCanonicalBilinearShellMean b y N u v k l Q ^ 2 ≤ conductorHarmonicFactor Q * (↑((vaughanCanonicalTensorLength y k).log2 + 1) ^ 2 * ↑(2 ^ k) * (↑(vaughanCanonicalTensorLength y k) + primitiveBilinearQFactor Q * ↑Q ^ 2) * (27 * B ^ 2 * (↑(2 ^ k) * ↑(vaughanCanonicalTensorLength y k)) * Real.log ↑(y + 1) ^ 5))

Fully explicit direct-shell square bound. In contrast with applying an additional rowwise estimate after Cauchy, the 27 tensor energy is multiplied only once.

theorem AnalyticNumberTheory.LargeSieve.bilinear_direct_shell_physical_scale (D M y Q c : ℝ) (hD : 0 ≤ D) (hM : 0 ≤ M) (hy : 0 ≤ y) (hQ : 0 ≤ Q) (hc : 0 ≤ c) (hDM : D * M ≤ y) : √(D * (M + c * Q ^ 2) * (D * M)) ≤ y + √c * Q * √(D * y)

Scalar physical-scale extraction from the square ledger. If X = D*M ≤ y, then the polynomial part of the direct shell is bounded by y + sqrt(c) Q sqrt(D*y). This is the point at which the apparent extra D*M is removed by taking the square root.

theorem AnalyticNumberTheory.LargeSieve.vaughanDirectAPNormalizedTypeIIInput_of_bilinear_shells {ι : Type u_1} [DecidableEq ι] (shells : Finset ι) (shellMean : ι → ℝ) (N Q u v : ℕ) (logPay : ℝ) (hdecomp : apNormalizedVaughanTypeIIMean N Q u v ≤ ∑ s ∈ shells, shellMean s) (hshell : ∀ s ∈ shells, shellMean s ≤ logPay * (↑N + ↑Q * ↑N / √↑(u + 1))) : VaughanDirectAPNormalizedTypeIIInput N Q u v (↑shells.card) logPay

Honest final wiring: once the exact canonical shell decomposition and its physical bounds have been proved, their finite sum inhabits the existing AP-normalized Type-II input. No Type-II estimate is assumed under another name.