Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.RankOneRectangularPrimitiveL1

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.

source
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
Instances For
    source
    theorem AnalyticNumberTheory.LargeSieve.rankOneRectangularWeightedPrimitiveMean_nonneg (a b : ℤ → ℂ) (Ma Mb : ℤ) (Na Nb : ℕ) (S : Finset ℕ) :
    0 ≤ rankOneRectangularWeightedPrimitiveMean a b Ma Mb Na Nb S
    source
    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.

    source
    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.

    source
    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
    Instances For
      source
      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.

      source
      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.