Rank-one rectangular primitive L¹ means

This leaf separates the elementary rectangular part of a Type-II first moment from the genuinely hyperbolic prefix problem. A rank-one rectangle is paid by two one-dimensional weighted primitive large sieves and one Cauchy--Schwarz inequality. The sole remaining interface says that an actual collected Vaughan hyperbolic shell is dominated by finitely many such rectangles.

This module is intentionally not imported by a canonical facade.

noncomputable def AnalyticNumberTheory.LargeSieve.rankOneRectangularWeightedPrimitiveMean (a b : ℤ → ℂ) (Ma Mb : ℤ) (Na Nb : ℕ) (S : Finset ℕ) : ℝ

Weighted primitive first moment of a rank-one rectangular character sum. The conductor set is explicit so the same theorem applies to one production conductor block.

Equations

• AnalyticNumberTheory.LargeSieve.rankOneRectangularWeightedPrimitiveMean a b Ma Mb Na Nb S = ∑ q ∈ S, ↑q / ↑q.totient * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖∑ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), a m * ↑χ ↑m‖ * ‖∑ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), b n * ↑χ ↑n‖

theorem AnalyticNumberTheory.LargeSieve.rankOneRectangularWeightedPrimitiveMean_nonneg (a b : ℤ → ℂ) (Ma Mb : ℤ) (Na Nb : ℕ) (S : Finset ℕ) : 0 ≤ rankOneRectangularWeightedPrimitiveMean a b Ma Mb Na Nb S

theorem AnalyticNumberTheory.LargeSieve.rankOneRectangularWeightedPrimitiveMean_sq_le (a b : ℤ → ℂ) (Ma Mb : ℤ) (Na Nb Q : ℕ) (hQ : 0 < Q) (S : Finset ℕ) (hS : S ⊆ Finset.Icc 1 Q) : rankOneRectangularWeightedPrimitiveMean a b Ma Mb Na Nb S ^ 2 ≤ (largeSieveBound Na (1 / ↑Q ^ 2) * ∑ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ‖a m‖ ^ 2) * (largeSieveBound Nb (1 / ↑Q ^ 2) * ∑ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), ‖b n‖ ^ 2)

The elementary rectangular theorem. After flattening the finite dependent family (q,χ), Cauchy gives two square ledgers; each is exactly one invocation of the one-dimensional weighted primitive large sieve.

theorem AnalyticNumberTheory.LargeSieve.rankOneRectangularWeightedPrimitiveMean_le (a b : ℤ → ℂ) (Ma Mb : ℤ) (Na Nb Q : ℕ) (hQ : 0 < Q) (S : Finset ℕ) (hS : S ⊆ Finset.Icc 1 Q) : rankOneRectangularWeightedPrimitiveMean a b Ma Mb Na Nb S ≤ √(largeSieveBound Na (1 / ↑Q ^ 2) * ∑ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ‖a m‖ ^ 2) * √(largeSieveBound Nb (1 / ↑Q ^ 2) * ∑ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), ‖b n‖ ^ 2)

Unsquared form convenient for finite shell assembly.

def AnalyticNumberTheory.LargeSieve.VaughanTypeIIHyperbolicSeparation {ι : Type u_1} [Fintype ι] (N u v k l : ℕ) (S : Finset ℕ) (left right : ι → ℤ → ℂ) (leftStart rightStart : ι → ℤ) (leftLength rightLength : ι → ℕ) : Prop

The unique analytic residual: separation of one actual hyperbolic collected shell into finitely many rank-one rectangles. Everything after this interface is the proved rectangular theorem above and finite summation.

Equations

• AnalyticNumberTheory.LargeSieve.VaughanTypeIIHyperbolicSeparation N u v k l S left right leftStart rightStart leftLength rightLength = (AnalyticNumberTheory.LargeSieve.blockWeightedVaughanActualCollectedShellMean N u v k l S ≤ ∑ i : ι, AnalyticNumberTheory.LargeSieve.rankOneRectangularWeightedPrimitiveMean (left i) (right i) (leftStart i) (rightStart i) (leftLength i) (rightLength i) S)

theorem AnalyticNumberTheory.LargeSieve.blockWeightedVaughanActualCollectedShellMean_le_of_hyperbolicSeparation {ι : Type u_1} [Fintype ι] (N u v k l Q : ℕ) (hQ : 0 < Q) (S : Finset ℕ) (hS : S ⊆ Finset.Icc 1 Q) (left right : ι → ℤ → ℂ) (leftStart rightStart : ι → ℤ) (leftLength rightLength : ι → ℕ) (hsep : VaughanTypeIIHyperbolicSeparation N u v k l S left right leftStart rightStart leftLength rightLength) : blockWeightedVaughanActualCollectedShellMean N u v k l S ≤ ∑ i : ι, √(largeSieveBound (leftLength i) (1 / ↑Q ^ 2) * ∑ m ∈ Finset.Icc (leftStart i + 1) (leftStart i + ↑(leftLength i)), ‖left i m‖ ^ 2) * √(largeSieveBound (rightLength i) (1 / ↑Q ^ 2) * ∑ n ∈ Finset.Icc (rightStart i + 1) (rightStart i + ↑(rightLength i)), ‖right i n‖ ^ 2)

A separated actual shell is paid solely by the two one-dimensional large sieves for each rank-one rectangle.

theorem AnalyticNumberTheory.LargeSieve.exactVaughanTypeII_blockWeighted_mean_le_of_hyperbolicSeparation {ι : Type u_1} [Fintype ι] (N u v Q : ℕ) (hQ : 0 < Q) (S : Finset ℕ) (hS : S ⊆ Finset.Icc 1 Q) (left right : ℕ × ℕ → ι → ℤ → ℂ) (leftStart rightStart : ℕ × ℕ → ι → ℤ) (leftLength rightLength : ℕ × ℕ → ι → ℕ) (hsep : ∀ kl ∈ vaughanTypeIIActiveCanonicalRectangles N u v, VaughanTypeIIHyperbolicSeparation N u v kl.1 kl.2 S (left kl) (right kl) (leftStart kl) (rightStart kl) (leftLength kl) (rightLength kl)) : typeIIBlockWeightedPrimitiveMean (vaughanTypeIICoeff vaughanUnitIntegerCoeff u v) N S ≤ ∑ kl ∈ vaughanTypeIIActiveCanonicalRectangles N u v, ∑ i : ι, √(largeSieveBound (leftLength kl i) (1 / ↑Q ^ 2) * ∑ m ∈ Finset.Icc (leftStart kl i + 1) (leftStart kl i + ↑(leftLength kl i)), ‖left kl i m‖ ^ 2) * √(largeSieveBound (rightLength kl i) (1 / ↑Q ^ 2) * ∑ n ∈ Finset.Icc (rightStart kl i + 1) (rightStart kl i + ↑(rightLength kl i)), ‖right kl i n‖ ^ 2)

Connection to the actual Vaughan fixed-conductor-block L¹ mean. The only premise not discharged by existing finite decomposition or one-dimensional large sieve is VaughanTypeIIHyperbolicSeparation, once for each active shell.