Global bound for Liu's AP prime-power correction

This module bounds the progression-restricted correction by the unrestricted nonprime von Mangoldt sum. On nonzero von Mangoldt support, n >= 2, so the normalizing logarithm is bounded below by the exact constant log 2.

noncomputable def MathlibNt.SieveTheory.LiuWeight.globalPrimePowerCorrection (y : ℕ) : ℝ

The unrestricted nonprime von Mangoldt sum with the logarithmic normalization occurring in the prime-power correction.

Equations

• MathlibNt.SieveTheory.LiuWeight.globalPrimePowerCorrection y = ∑ n ∈ Finset.range (y + 1), if Nat.Prime n then 0 else ArithmeticFunction.vonMangoldt n / Real.log ↑n

theorem MathlibNt.SieveTheory.LiuWeight.apPrimePowerCorrection_le_global (y q l : ℕ) : AnalyticNumberTheory.Sieve.apPrimePowerCorrection y q l ≤ globalPrimePowerCorrection y

Removing the congruence restriction only enlarges the nonnegative prime-power correction. This includes the degenerate moduli q = 0, 1.

theorem MathlibNt.SieveTheory.LiuWeight.apPrimePowerCorrection_mod_one (y l : ℕ) : AnalyticNumberTheory.Sieve.apPrimePowerCorrection y 1 l = globalPrimePowerCorrection y

Modulo one the progression restriction disappears exactly.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePower_modulusWeight_zero : ↑(ArithmeticFunction.moebius 0) ^ 2 * 3 ^ (Nat.primeFactors 0).card = 0

The zero-modulus term in Liu's outer average is killed by its squared Möbius weight, independently of the residue convention modulo zero.

theorem MathlibNt.SieveTheory.LiuWeight.globalPrimePowerCorrection_le_psi_sub_theta (y : ℕ) : globalPrimePowerCorrection y ≤ (Chebyshev.psi ↑y - Chebyshev.theta ↑y) / Real.log 2

The unrestricted correction is at most the Chebyshev prime-power tail divided by the exact lower bound log 2 for its denominator.

theorem MathlibNt.SieveTheory.LiuWeight.apPrimePowerCorrection_le_psi_sub_theta (y q l : ℕ) : AnalyticNumberTheory.Sieve.apPrimePowerCorrection y q l ≤ (Chebyshev.psi ↑y - Chebyshev.theta ↑y) / Real.log 2

The AP correction is bounded by the same Chebyshev tail, uniformly in the modulus and residue.

theorem MathlibNt.SieveTheory.LiuWeight.globalPrimePowerCorrection_nonneg (y : ℕ) : 0 ≤ globalPrimePowerCorrection y

The global correction is nonnegative, including at y = 0, 1.

theorem MathlibNt.SieveTheory.LiuWeight.exists_globalPrimePowerCorrection_le_sqrt : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (y : ℕ), globalPrimePowerCorrection y ≤ C * √↑y

Effective Chebyshev control gives a nonnegative constant for which the global logarithmically normalized correction is O(sqrt y).

theorem MathlibNt.SieveTheory.LiuWeight.globalPrimePowerCorrection_isBigO_sqrt : globalPrimePowerCorrection =O[Filter.atTop] fun (y : ℕ) => √↑y

Asymptotic form of the effective global correction bound.

Lifting the global estimate through Liu's finite maxima

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerSqrtSupport (y X : ℕ) (f : ℕ → ℝ) : ℝ

The exact Liu-weight support functional left by the global square-root estimate. The source weight is retained as |f a|.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerSqrtSupport y X f = ∑ a ∈ Finset.Icc 1 X, |f a| * √↑(y / a)

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPairSqrtMass (N : ℕ) : ℝ

The square-root mass of Liu's exact source pair set.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPairSqrtMass N = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.liuWeightPairs N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N), √↑(N / (p.1 * p.2))

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerSqrtSupport_source_eq_pairSqrtMass (N : ℕ) : liuPanPrimePowerSqrtSupport N N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) = liuPanPrimePowerPairSqrtMass N

For Liu's characteristic source weight, the support functional is exactly the square-root mass of the unique admissible prime-pair representations.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPairSqrtMass_sq_le (N : ℕ) : liuPanPrimePowerPairSqrtMass N ^ 2 ≤ ↑(liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N)).card * (↑N * liuWeightPairReciprocalSum N)

Cauchy--Schwarz reduces the source pair square-root mass to the exact pair cardinality and the already controlled reciprocal pair mass.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerSqrtSupport_nonneg (y X : ℕ) (f : ℕ → ℝ) : 0 ≤ liuPanPrimePowerSqrtSupport y X f

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerSqrtSupport_mono {y x X : ℕ} (hyx : y ≤ x) (f : ℕ → ℝ) : liuPanPrimePowerSqrtSupport y X f ≤ liuPanPrimePowerSqrtSupport x X f

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSignedCorrectionKernel_le_global (y a q l : ℕ) : liuPanSignedCorrectionKernel y a q l ≤ globalPrimePowerCorrection (y / a)

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSignedCorrectionBound_le_global (y X q l : ℕ) (f : ℕ → ℝ) : liuPanSignedCorrectionBound y X q l f ≤ ∑ a ∈ Finset.Icc 1 X, |f a| * globalPrimePowerCorrection (y / a)

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSignedCorrectionBound_le_sqrtSupport {C : ℝ} (hglobal : ∀ (t : ℕ), globalPrimePowerCorrection t ≤ C * √↑t) (y X q l : ℕ) (f : ℕ → ℝ) : liuPanSignedCorrectionBound y X q l f ≤ C * liuPanPrimePowerSqrtSupport y X f

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAPPrimePowerCorrectionMaxL_le_sqrtSupport {C : ℝ} (hC : 0 ≤ C) (hglobal : ∀ (t : ℕ), globalPrimePowerCorrection t ≤ C * √↑t) (y X q : ℕ) (f : ℕ → ℝ) : liuPanAPPrimePowerCorrectionMaxL y X q f ≤ C * liuPanPrimePowerSqrtSupport y X f

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAPPrimePowerCorrectionMaxY_le_sqrtSupport {C : ℝ} (hC : 0 ≤ C) (hglobal : ∀ (t : ℕ), globalPrimePowerCorrection t ≤ C * √↑t) (X q x : ℕ) (f : ℕ → ℝ) : liuPanAPPrimePowerCorrectionMaxY X q x f ≤ C * liuPanPrimePowerSqrtSupport x X f

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeightMass (N : ℕ) (B : ℝ) : ℝ

The exact finite support and modulus-weight functional remaining after the global Chebyshev estimate. No bound on the source weight is inserted here.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeightMass N B = ∑ q ∈ Finset.range (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuMainPanPrimePowerSqrtSupport (N : ℕ) (f : ℕ → ℝ) (B : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainPanPrimePowerSqrtSupport N f B = ∑ q ∈ Finset.range (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerSqrtSupport N N f

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanPrimePowerSqrtSupport_eq_mul (N : ℕ) (f : ℕ → ℝ) (B : ℝ) : liuMainPanPrimePowerSqrtSupport N f B = liuPanPrimePowerModulusWeightMass N B * liuPanPrimePowerSqrtSupport N N f

The remaining global-support functional factors exactly into a modulus weight mass and the source support mass.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanPrimePowerSqrtSupport_source_eq_mul (N : ℕ) (B : ℝ) : liuMainPanPrimePowerSqrtSupport N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) B = liuPanPrimePowerModulusWeightMass N B * liuPanPrimePowerPairSqrtMass N

Source specialization of the exact factorization: the only remaining inputs are the modulus weight mass and Liu's pair square-root mass.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanAPPrimePowerCorrection_average_le_sqrtSupport {C : ℝ} (hC : 0 ≤ C) (hglobal : ∀ (t : ℕ), globalPrimePowerCorrection t ≤ C * √↑t) (N : ℕ) (f : ℕ → ℝ) (B : ℝ) : ∑ q ∈ Finset.range (panModulusCutoff N B + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * liuPanAPPrimePowerCorrectionMaxY N q N f ≤ C * liuMainPanPrimePowerSqrtSupport N f B

theorem MathlibNt.SieveTheory.LiuWeight.LiuMainPanAPPrimePowerCorrectionBoundAt.of_sqrtSupport {C K : ℝ} (hC : 0 ≤ C) (hglobal : ∀ (t : ℕ), globalPrimePowerCorrection t ≤ C * √↑t) {N : ℕ} {f : ℕ → ℝ} {A B : ℝ} (hsupport : liuMainPanPrimePowerSqrtSupport N f B ≤ K * ↑N / Real.log ↑N ^ A) : LiuMainPanAPPrimePowerCorrectionBoundAt N f A B (C * K)

An explicit bound for the remaining finite support functional is exactly the additional input needed to close the existing fixed-N correction bound.