Damped-arctangent rectangular hyperbolic primitive means

This leaf states the rectangular smoothed-kernel primitive mean and its two quantitative endpoints. It combines the exact Ioi damped Perron formula, the finite two-term rank-one separation, the weighted rectangular primitive large sieve, and the explicit damped-majorant integral.

noncomputable def AnalyticNumberTheory.LargeSieve.rectangularSmoothedKernelCharacterSum (a b : ℤ → ℂ) (ε y : ℝ) (Ma Mb : ℤ) (Na Nb q : ℕ) (χ : PrimitiveCharacter q) : ℂ

A rectangular character sum weighted by the damped Perron step kernel.

Equations

• AnalyticNumberTheory.LargeSieve.rectangularSmoothedKernelCharacterSum a b ε y Ma Mb Na Nb q χ = ∑ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ∑ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), a m * b n * ↑χ ↑(m * n) * ↑(AnalyticNumberTheory.LargeSieve.dampedArctanPerronKernel ε (Real.log (y / ↑(m * n))))

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

Weighted primitive first moment of the smoothed rectangular kernel.

Equations

• AnalyticNumberTheory.LargeSieve.rectangularSmoothedKernelWeightedPrimitiveMean a b ε y Ma Mb Na Nb S = ∑ q ∈ S, ↑q / ↑q.totient * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖AnalyticNumberTheory.LargeSieve.rectangularSmoothedKernelCharacterSum a b ε y Ma Mb Na Nb q χ‖

noncomputable def AnalyticNumberTheory.LargeSieve.rectangularSharpHyperbolicCharacterSum (a b : ℤ → ℂ) (Y : ℕ) (Ma Mb : ℤ) (Na Nb q : ℕ) (χ : PrimitiveCharacter q) : ℂ

The corresponding sharp hyperbolic-indicator character sum.

Equations

• AnalyticNumberTheory.LargeSieve.rectangularSharpHyperbolicCharacterSum a b Y Ma Mb Na Nb q χ = ∑ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ∑ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), a m * b n * ↑χ ↑(m * n) * if m * n ≤ ↑Y then 1 else 0

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

Weighted primitive first moment with the sharp hyperbolic indicator.

Equations

• AnalyticNumberTheory.LargeSieve.rectangularSharpHyperbolicWeightedPrimitiveMean a b Y Ma Mb Na Nb S = ∑ q ∈ S, ↑q / ↑q.totient * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖AnalyticNumberTheory.LargeSieve.rectangularSharpHyperbolicCharacterSum a b Y Ma Mb Na Nb q χ‖

noncomputable def AnalyticNumberTheory.LargeSieve.rankOneRectangularLSRHS (a b : ℤ → ℂ) (Ma Mb : ℤ) (Na Nb Q : ℕ) : ℝ

The original rank-one large-sieve right hand side.

Equations

• AnalyticNumberTheory.LargeSieve.rankOneRectangularLSRHS a b Ma Mb Na Nb Q = √(AnalyticNumberTheory.LargeSieve.largeSieveBound Na (1 / ↑Q ^ 2) * ∑ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ‖a m‖ ^ 2) * √(AnalyticNumberTheory.LargeSieve.largeSieveBound Nb (1 / ↑Q ^ 2) * ∑ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), ‖b n‖ ^ 2)

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

Explicit coefficient L¹ mass of the rectangle.

Equations

• AnalyticNumberTheory.LargeSieve.rectangularCoefficientL1 a b Ma Mb Na Nb = (∑ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ‖a m‖) * ∑ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), ‖b n‖

noncomputable def AnalyticNumberTheory.LargeSieve.weightedPrimitiveFamilyMass (S : Finset ℕ) : ℝ

Explicit weighted mass of the primitive-character family.

Equations

• AnalyticNumberTheory.LargeSieve.weightedPrimitiveFamilyMass S = ∑ q ∈ S, ↑q / ↑q.totient * ↑(Fintype.card (AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q))

theorem AnalyticNumberTheory.LargeSieve.rectangularSmoothedKernelWeightedPrimitiveMean_le (a b : ℤ → ℂ) (y : ℝ) (Ma Mb : ℤ) (Na Nb Q M : ℕ) (hQ : 0 < Q) (S : Finset ℕ) (hS : S ⊆ Finset.Icc 1 Q) (hM : 3 ≤ M) (hy0 : 1 / 2 ≤ y) (hyM : y ≤ ↑M + 1 / 2) (hm1 : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), 1 ≤ m) (hmM : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), m ≤ ↑M) (hn1 : ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), 1 ≤ n) (hnM : ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), n ≤ ↑M) : rectangularSmoothedKernelWeightedPrimitiveMean a b (1 / ↑M ^ 2) y Ma Mb Na Nb S ≤ (1 / 2 + (7 * Real.log ↑M + 2) / Real.pi) * rankOneRectangularLSRHS a b Ma Mb Na Nb Q

For ε=M⁻², positive rectangular supports bounded by M, and a half-step parameter in [1/2,M+1/2], the smoothed mean is bounded by the original rank-one LS right hand side. The constants 2 log M, log M from the two sine lanes contribute respectively 4 log M+1, 3 log M+1 under dampedPerronMajorant_integral_Ioi_le, hence 7 log M+2 in total.

theorem AnalyticNumberTheory.LargeSieve.rectangularSharpHyperbolicWeightedPrimitiveMean_le_smoothed (a b : ℤ → ℂ) (Y M : ℕ) (Ma Mb : ℤ) (Na Nb : ℕ) (S : Finset ℕ) (hM : 1 ≤ M) (hYM : Y ≤ M) (hmnPos : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), 0 < m * n) (_hmnM : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), m * n ≤ ↑M) : rectangularSharpHyperbolicWeightedPrimitiveMean a b Y Ma Mb Na Nb S ≤ rectangularSmoothedKernelWeightedPrimitiveMean a b (1 / ↑M ^ 2) (MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep Y) Ma Mb Na Nb S + 8 / (Real.pi * ↑M) * rectangularCoefficientL1 a b Ma Mb Na Nb * weightedPrimitiveFamilyMass S

Sharp-to-smoothed comparison with the error displayed explicitly. The product-support bound is the exact hyperbolic support condition used to apply the half-step separation lemma to the integer m*n.