Prefix-maximal explicit bilinear tensor estimate

This independent leaf upgrades the explicit nonmaximal bilinear tensor estimate to the complete maximum over the collected t-prefix. The aligned dyadic Rademacher--Menshov decomposition in DyadicPrefixMaximal pays exactly (Nat.log2 M + 1)^2; Cauchy in the outer row variable does not move the maximum outside the primitive-character sum.

noncomputable def AnalyticNumberTheory.LargeSieve.bilinearTensorCharacterPrefixSquare (A : ℕ → ℤ → ℂ) (DS : Finset ℕ) (y q : ℕ) (χ : PrimitiveCharacter q) : ℝ

Square of the bilinear tensor form truncated at the collected-variable prefix 1 ≤ t ≤ y.

Equations

• AnalyticNumberTheory.LargeSieve.bilinearTensorCharacterPrefixSquare A DS y q χ = ‖∑ d ∈ DS, ∑ t ∈ Finset.Icc 1 ↑y, A d t * ↑χ (↑↑d * ↑t)‖ ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.bilinearTensorCharacterPrefixMaxSquare (A : ℕ → ℤ → ℂ) (DS : Finset ℕ) (M q : ℕ) (χ : PrimitiveCharacter q) : ℝ

Complete t-prefix maximum for a bilinear tensor form.

Equations

• AnalyticNumberTheory.LargeSieve.bilinearTensorCharacterPrefixMaxSquare A DS M q χ = (Finset.image (fun (y : ℕ) => AnalyticNumberTheory.LargeSieve.bilinearTensorCharacterPrefixSquare A DS y q χ) (Finset.range (M + 1))).max' ⋯

theorem AnalyticNumberTheory.LargeSieve.bilinearTensorCharacterPrefixMaxSquare_nonneg (A : ℕ → ℤ → ℂ) (DS : Finset ℕ) (M q : ℕ) (χ : PrimitiveCharacter q) : 0 ≤ bilinearTensorCharacterPrefixMaxSquare A DS M q χ

theorem AnalyticNumberTheory.LargeSieve.bilinearTensorCharacterPrefixMaxSquare_le_rows (A : ℕ → ℤ → ℂ) (DS : Finset ℕ) (M q : ℕ) (χ : PrimitiveCharacter q) : bilinearTensorCharacterPrefixMaxSquare A DS M q χ ≤ ↑DS.card * ∑ d ∈ DS, primitiveCharacterPrefixMaxSquare (A d) 0 M q χ

Every complete bilinear prefix maximum is bounded by outer-row Cauchy and the sum of the complete row-prefix maxima.

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_bilinearTensor_prefixMax_explicit (A : ℕ → ℤ → ℂ) (DS : Finset ℕ) (D M Q : ℕ) (hQ : 0 < Q) (hcard : DS.card ≤ D) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, bilinearTensorCharacterPrefixMaxSquare A DS M q χ ≤ ↑(M.log2 + 1) ^ 2 * ↑D * (↑M + primitiveBilinearQFactor Q * ↑Q ^ 2) * bilinearTensorCoeffEnergy A DS M

Generic explicit t-prefix-maximal bilinear tensor theorem. The aligned dyadic decomposition is applied to each row and costs exactly (log₂ M + 1)^2; the remaining factor is the already proved Q-dependent nonmaximal constant D * (M + c(Q)Q^2).

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanCanonicalBilinearPrefixMaxSquare (b : ℕ → ℂ) (y N u v k l q : ℕ) (χ : PrimitiveCharacter q) : ℝ

The canonical Vaughan Type-II block with the complete collected-variable prefix maximum, at the physical short length y / 2^k.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanCanonicalBilinearPrefixMaxSquare b y N u v k l q χ = AnalyticNumberTheory.LargeSieve.bilinearTensorCharacterPrefixMaxSquare (AnalyticNumberTheory.LargeSieve.vaughanCanonicalBilinearTensor b y N v l) (AnalyticNumberTheory.LargeSieve.vaughanCanonicalDyadicBlock N u k) (AnalyticNumberTheory.LargeSieve.vaughanCanonicalTensorLength y k) q χ

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanCanonicalBilinear_prefixMax_unconditional (b : ℕ → ℂ) (y N u v k l Q : ℕ) (hQ : 0 < Q) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, vaughanCanonicalBilinearPrefixMaxSquare b y N u v k l 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

Canonical complete-prefix theorem, with no fourth-moment premise.

theorem AnalyticNumberTheory.LargeSieve.imprimitive_conductor_window_vaughanCanonicalBilinear_prefixMax (b : ℕ → ℂ) (y N Q C u v k l : ℕ) (hC : 0 < C) : ∑ d ∈ Finset.Icc C (2 * C), imprimitiveConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, vaughanCanonicalBilinearPrefixMaxSquare b y N u v k l d ψ ≤ ↑(Q / C) * conductorHarmonicFactor (Q / C) * (↑((vaughanCanonicalTensorLength y k).log2 + 1) ^ 2 * ↑(2 ^ k) * (↑(vaughanCanonicalTensorLength y k) + primitiveBilinearQFactor (2 * C) * ↑(2 * C) ^ 2) * vaughanCanonicalShortTensorEnergy vaughanMangoldtCoeff b y N u v k l)

Linear-harmonic imprimitive conductor-window transport for the complete canonical bilinear prefix maximum.

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanCanonicalBilinear_prefixMax_energy27 (b : ℕ → ℂ) (y N u v k l Q : ℕ) (B : ℝ) (hQ : 0 < Q) (hB : ∀ n ≤ y, ‖b n‖ ≤ B) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, vaughanCanonicalBilinearPrefixMaxSquare b y N u v k l 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)

Substitution of the explicit divisor-square constant 27. This theorem makes the remaining full row-mass factor visible.

theorem AnalyticNumberTheory.LargeSieve.bilinear_prefix_energy27_scale_audit (D M Q L : ℝ) : D * (M + Q ^ 2) * (27 * (D * M) * L) = 27 * (D * M) * (D * M + D * Q ^ 2) * L

Algebraic audit: after writing X=D*M, the prefix maximal route with the 27-energy still contains X * (X + D*Q^2). Thus the dyadic maximal upgrade does not itself supply the missing N/log saving needed by a BV endpoint.