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.rectangularDampedPerron_integrable_formula (a b : ℤ → ℂ) (ε y : ℝ) (hε : 0 < ε) (Ma Mb : ℤ) (Na Nb q : ℕ) (χ : PrimitiveCharacter q) : MeasureTheory.IntegrableOn (fun (t : ℝ) => ↑(Real.exp (-ε * t)) * rectangularKernelCharacterSum a b y t Ma Mb Na Nb q χ) (Set.Ioi 0) MeasureTheory.volume ∧ rectangularSmoothedKernelCharacterSum a b ε y Ma Mb Na Nb q χ = 1 / 2 * ((∑ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), a m * ↑χ ↑m) * ∑ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), b n * ↑χ ↑n) + 1 / ↑Real.pi * ∫ (t : ℝ) in Set.Ioi 0, ↑(Real.exp (-ε * t)) * rectangularKernelCharacterSum a b y t Ma Mb Na Nb q χ

Exact damped Perron interchange, before any character mean estimate. The real cutoff is arbitrary, so the same identity applies to each selector value.

theorem AnalyticNumberTheory.LargeSieve.rankOneRectangularWeightedPrimitiveMean_le_scaled_energy (a b c d : ℤ → ℂ) (Ma Mb : ℤ) (Na Nb Q : ℕ) (hQ : 0 < Q) (S : Finset ℕ) (hS : S ⊆ Finset.Icc 1 Q) (u v : ℝ) (hu : 0 ≤ u) (hv : 0 ≤ v) (hc : ∑ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ‖c m‖ ^ 2 ≤ u ^ 2 * ∑ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ‖a m‖ ^ 2) (hd : ∑ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), ‖d n‖ ^ 2 ≤ v ^ 2 * ∑ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), ‖b n‖ ^ 2) : rankOneRectangularWeightedPrimitiveMean c d Ma Mb Na Nb S ≤ u * v * rankOneRectangularLSRHS a b Ma Mb Na Nb Q

Two-sided energy scaling of the original aggregated rank-one large sieve. No estimate of individual character sums is substituted for this mean.

theorem AnalyticNumberTheory.LargeSieve.dampedPerron_weighted_norm_integrable (S : Finset ℕ) (w : ℕ → ℝ) (F : (q : ℕ) → PrimitiveCharacter q → ℝ → ℂ) (μ : MeasureTheory.Measure ℝ) (hF : ∀ (q : ℕ) (χ : PrimitiveCharacter q), MeasureTheory.Integrable (F q χ) μ) : MeasureTheory.Integrable (fun (t : ℝ) => ∑ q ∈ S, w q * ∑ χ : PrimitiveCharacter q, ‖F q χ t‖) μ

Integrability of the weighted primitive first moment.

theorem AnalyticNumberTheory.LargeSieve.dampedPerron_weighted_norm_integral_le (S : Finset ℕ) (w : ℕ → ℝ) (hw : ∀ q ∈ S, 0 ≤ w q) (F : (q : ℕ) → PrimitiveCharacter q → ℝ → ℂ) (μ : MeasureTheory.Measure ℝ) (hF : ∀ (q : ℕ) (χ : PrimitiveCharacter q), MeasureTheory.Integrable (F q χ) μ) : ∑ q ∈ S, w q * ∑ χ : PrimitiveCharacter q, ‖∫ (t : ℝ), F q χ t ∂μ‖ ≤ ∫ (t : ℝ), ∑ q ∈ S, w q * ∑ χ : PrimitiveCharacter q, ‖F q χ t‖ ∂μ

Norm/integral interchange for the actual weighted primitive family.

theorem AnalyticNumberTheory.LargeSieve.dampedPerron_weighted_norm_add_le (S : Finset ℕ) (w : ℕ → ℝ) (hw : ∀ q ∈ S, 0 ≤ w q) (D I : (q : ℕ) → PrimitiveCharacter q → ℂ) (p r : ℝ) (hp : 0 ≤ p) (hr : 0 ≤ r) : ∑ q ∈ S, w q * ∑ χ : PrimitiveCharacter q, ‖↑p * D q χ + ↑r * I q χ‖ ≤ p * ∑ q ∈ S, w q * ∑ χ : PrimitiveCharacter q, ‖D q χ‖ + r * ∑ q ∈ S, w q * ∑ χ : PrimitiveCharacter q, ‖I q χ‖

Weighted norm subadditivity with the two real prefactors pulled out. This is used only after the exact Perron identity, not to replace a rank-one mean.

theorem AnalyticNumberTheory.LargeSieve.dampedPerron_integral_le_two_majorants {ε L₁ L₂ R : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hL₁ : 0 ≤ L₁) (hL₂ : 0 ≤ L₂) (hR : 0 ≤ R) {G : ℝ → ℝ} (hGint : MeasureTheory.IntegrableOn G (Set.Ioi 0) MeasureTheory.volume) (hG : ∀ t ∈ Set.Ioi 0, G t ≤ (dampedPerronMajorantIntegrand ε L₁ t + dampedPerronMajorantIntegrand ε L₂ t) * R) : ∫ (t : ℝ) in Set.Ioi 0, G t ≤ (L₁ + Real.log (1 / ε) + 1 + (L₂ + Real.log (1 / ε) + 1)) * R

Integrate a two-frequency damped majorant without any sign assumption on its integrable minorant. Multiplicity of equal lanes is absorbed into R.

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.rectangularSharpHyperbolicCharacterSum_norm_le_smoothed (a b : ℤ → ℂ) (Y M : ℕ) (Ma Mb : ℤ) (Na Nb : ℕ) (hM : 1 ≤ M) (hYM : Y ≤ M) (hmnPos : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), 0 < m * n) (q : ℕ) (χ : PrimitiveCharacter q) : ‖rectangularSharpHyperbolicCharacterSum a b Y Ma Mb Na Nb q χ‖ ≤ ‖rectangularSmoothedKernelCharacterSum a b (1 / ↑M ^ 2) (MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep Y) Ma Mb Na Nb q χ‖ + 8 / (Real.pi * ↑M) * rectangularCoefficientL1 a b Ma Mb Na Nb

The half-step smoothing error for one rectangular character sum. The cutoff remains an argument, so it may later depend on the character.

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 hypothesis is retained for compatibility; the half-step separation argument does not require this upper bound on m*n.