Character form of Liu's prime-power correction

The coefficient below records every admissible ordered Liu pair and every prime-power correction factor separately. Thus no multiplicity is lost before the progression condition is converted to characters.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerKappa (m : ℕ) : ℝ

The nonnegative non-prime part of the logarithmically normalized von Mangoldt function.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerKappa m = if Nat.Prime m then 0 else ArithmeticFunction.vonMangoldt m / Real.log ↑m

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

The finite multiplicity-preserving coefficient obtained from Liu's ordered prime-pair source and the non-prime von Mangoldt correction.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient N n = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.liuWeightPairs N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N), ∑ m ∈ Finset.range (N + 1), if p.1 * p.2 * m = n then MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerKappa m else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerAPSum (N y q l : ℕ) : ℝ

The progression partial sum of the multiplicity-preserving coefficient.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerAPSum N y q l = ∑ n ∈ Finset.range (y + 1), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient N n * if n ≡ l [MOD q] then 1 else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerSourceAPSum (N y q l : ℕ) : ℝ

The same AP sum before the finite product coefficient is collected.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerSourceAPSum N y q l = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.liuWeightPairs N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N), ∑ m ∈ Finset.range (N + 1), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerKappa m * if p.1 * p.2 * m ≤ y ∧ p.1 * p.2 * m ≡ l [MOD q] then 1 else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoprimeSourceAPSum (N y q l : ℕ) : ℝ

The source AP sum with the coprimality gate appearing in Liu's signed correction bound still displayed.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoprimeSourceAPSum N y q l = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.liuWeightPairs N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N), if (p.1 * p.2).Coprime q then ∑ m ∈ Finset.range (N + 1), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerKappa m * if p.1 * p.2 * m ≤ y ∧ p.1 * p.2 * m ≡ l [MOD q] then 1 else 0 else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCharacterMean (N y q l : ℕ) : ℂ

The full character mean attached to the coefficient AP sum.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCharacterMean N y q l = (↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q, star (χ ↑l) * ∑ n ∈ Finset.range (y + 1), ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient N n) * χ ↑n

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

The unprogressed coefficient mass through y.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerTotal N y = ∑ n ∈ Finset.range (y + 1), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient N n

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoprimeTotal (N y q : ℕ) : ℝ

The coefficient mass through y on integers coprime to q. This is the mass selected by the principal Dirichlet character modulo q.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoprimeTotal N y q = ∑ n ∈ Finset.range (y + 1), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient N n * if n.Coprime q then 1 else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNoncoprimeTotal (N y q : ℕ) : ℝ

The complementary coefficient mass through y on nonunits modulo q.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNoncoprimeTotal N y q = ∑ n ∈ Finset.range (y + 1), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient N n * if n.Coprime q then 0 else 1

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerDiscrepancy (N y q l : ℕ) : ℝ

The real character discrepancy: the real part of the full character mean minus its principal density contribution.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerDiscrepancy N y q l = (MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCharacterMean N y q l).re - MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerTotal N y / ↑q.totient

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalDiscrepancy (N y q l : ℕ) : ℝ

The genuine nonprincipal discrepancy: the AP sum minus the mass selected by the principal character, divided by φ(q).

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalDiscrepancy N y q l = MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerAPSum N y q l - MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoprimeTotal N y q / ↑q.totient

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerKappa_nonneg (m : ℕ) : 0 ≤ liuPanPrimePowerKappa m

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerKappa_le_one (m : ℕ) : liuPanPrimePowerKappa m ≤ 1

The normalized non-prime von Mangoldt contribution is at most one.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient_nonneg (N n : ℕ) : 0 ≤ liuPanPrimePowerCoefficient N n

Every coefficient is nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient_le_primeFactors_sq (N n : ℕ) : liuPanPrimePowerCoefficient N n ≤ ↑n.primeFactors.card ^ 2

The number of ordered nonzero source representations of n is at most the square of the number of distinct prime divisors of n.

theorem MathlibNt.SieveTheory.LiuWeight.primeFactors_card_cast_le_log {n : ℕ} (hn : 2 ≤ n) : ↑n.primeFactors.card ≤ Real.log ↑n / Real.log 2

The standard elementary bound ω(n) ≤ log n / log 2.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient_le_log_sq (N n : ℕ) : liuPanPrimePowerCoefficient N n ≤ 1 + (Real.log ↑(n + 1) / Real.log 2) ^ 2

Pointwise polylogarithmic multiplicity bound for the collected source coefficient.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient_sq_sum_le (N : ℕ) : ∑ n ∈ Finset.range (N + 1), liuPanPrimePowerCoefficient N n ^ 2 ≤ (1 + (Real.log ↑(N + 1) / Real.log 2) ^ 2) * liuPanPrimePowerTotal N N

The exact L² ≤ L∞ · L¹ reduction for Liu's collected coefficients, with the pointwise multiplicity supplied by the logarithmic bound above.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient_eq_zero_of_sq_lt {N n : ℕ} (hn : N * N < n) : liuPanPrimePowerCoefficient N n = 0

The coefficient has the explicit finite support supplied by its two finite index sets.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient_eq_zero_of_lt {N n : ℕ} (hn : N * N < n) : liuPanPrimePowerCoefficient N n = 0

The coefficient sequence is finitely supported, with the transparent support cutoff N².

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePower_mem_range_mul_iff {N y a m : ℕ} (hy : y ≤ N) (ha : 0 < a) : m ∈ Finset.range (y / a + 1) ↔ m ∈ {m ∈ Finset.range (N + 1) | a * m ≤ y}

The exact floor-division audit needed when a source factor is absorbed into the prime-power variable.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePower_mul_mod_iff {a m q l : ℕ} (hcop : a.Coprime q) : a * m ≡ l [MOD q] ↔ m ≡ AnalyticNumberTheory.Sieve.natInvMod q a * l % q [MOD q]

The inverse-residue convention in the correction kernel is exactly the congruence obtained after restoring the source factor.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePower_coprime_of_mul_modEq {a m q l : ℕ} (hl : IsUnit ↑l) (hmod : a * m ≡ l [MOD q]) : a.Coprime q

A unit product residue forces the Liu source factor to be coprime to the modulus. This is the step which makes the unrestricted collected coefficient compatible with the coprime source sum.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCorrectionKernel_eq_productSum {N y a q l : ℕ} (hy : y ≤ N) (ha : 0 < a) (hcop : a.Coprime q) : liuPanSignedCorrectionKernel y a q l = ∑ m ∈ Finset.range (N + 1), liuPanPrimePowerKappa m * if a * m ≤ y ∧ a * m ≡ l [MOD q] then 1 else 0

Exact one-source-factor regrouping of the correction kernel. The proof uses both the floor-division and inverse-residue audits above.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSignedCorrectionBound_eq_coprimeSourceAPSum {N y q l : ℕ} (hy : y ≤ N) : liuPanSignedCorrectionBound y N q l (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) = liuPanPrimePowerCoprimeSourceAPSum N y q l

Reindexing the characteristic Liu weight by its unique source pair turns the correction bound into the coprime source AP sum.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoprimeSourceAPSum_eq_sourceAPSum {N y q l : ℕ} (hl : IsUnit ↑l) : liuPanPrimePowerCoprimeSourceAPSum N y q l = liuPanPrimePowerSourceAPSum N y q l

A unit target residue makes the coprimality gate in the source AP sum redundant, since a non-unit source factor cannot produce that residue.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerAPSum_eq_sourceAPSum (N y q l : ℕ) : liuPanPrimePowerAPSum N y q l = liuPanPrimePowerSourceAPSum N y q l

Collecting the finite coefficient back into its source pairs is exact; in particular every product collision retains its multiplicity.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSignedCorrectionBound_eq_apSum {N y q l : ℕ} (hy : y ≤ N) (hl : IsUnit ↑l) : liuPanSignedCorrectionBound y N q l (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) = liuPanPrimePowerAPSum N y q l

For y ≤ N and a unit residue, Liu's exact prime-power correction is the AP partial sum of the finite multiplicity-preserving coefficient.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCharacterMean_eq_apSum {N y q l : ℕ} (hq : 0 < q) (hl : IsUnit ↑l) : liuPanPrimePowerCharacterMean N y q l = ↑(liuPanPrimePowerAPSum N y q l)

The complex character mean is exactly the complexification of the AP partial sum.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCharacterMean_re_eq_apSum {N y q l : ℕ} (hq : 0 < q) (hl : IsUnit ↑l) : (liuPanPrimePowerCharacterMean N y q l).re = liuPanPrimePowerAPSum N y q l

The real part of the character mean is the real AP partial sum.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalCharacterMean (N y q l : ℕ) : ℂ

The character sum with the principal character removed.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalCharacterMean N y q l = (↑q.totient)⁻¹ * ∑ χ ∈ Finset.univ.erase 1, star (χ ↑l) * ∑ n ∈ Finset.range (y + 1), ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient N n) * χ ↑n

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrincipalCharacterTerm_eq_coprimeTotal (N y q : ℕ) : ∑ n ∈ Finset.range (y + 1), ↑(liuPanPrimePowerCoefficient N n) * 1 ↑n = ↑(liuPanPrimePowerCoprimeTotal N y q)

The principal character selects exactly the coefficient mass on units.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalDiscrepancy_eq_re_nonprincipalCharacterMean {N y q l : ℕ} (hq : 0 < q) (hl : IsUnit ↑l) : liuPanPrimePowerNonprincipalDiscrepancy N y q l = (liuPanPrimePowerNonprincipalCharacterMean N y q l).re

The genuine discrepancy is the real part of the normalized sum over nonprincipal characters, with the principal mass removed exactly.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalCharacterSquareSum (N y q l : ℕ) : ℝ

The exact square sum over the nonprincipal characters at a fixed cutoff.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalCharacterSquareSum N y q l = ∑ χ ∈ Finset.univ.erase 1, ‖star (χ ↑l) * ∑ n ∈ Finset.range (y + 1), ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient N n) * χ ↑n‖ ^ 2

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalCharacterCount (q : ℕ) : ℕ

The finite number of nonprincipal characters used in the square-sum bound.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalCharacterCount q = (Finset.univ.erase 1).card

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalDiscrepancy_abs_le_cauchySchwarz {N y q l : ℕ} (hq : 0 < q) (hl : IsUnit ↑l) : |liuPanPrimePowerNonprincipalDiscrepancy N y q l| ≤ (↑q.totient)⁻¹ * √↑(liuPanPrimePowerNonprincipalCharacterCount q) * √(liuPanPrimePowerNonprincipalCharacterSquareSum N y q l)

A pointwise absolute Cauchy--Schwarz bound for the bridge, with the all-nonprincipal square sum left explicit and no large-sieve estimate.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerTotal_eq_coprime_add_noncoprime (N y q : ℕ) : liuPanPrimePowerTotal N y = liuPanPrimePowerCoprimeTotal N y q + liuPanPrimePowerNoncoprimeTotal N y q

The unrestricted mass is the disjoint sum of its unit and nonunit parts.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoprimeTotal_nonneg (N y q : ℕ) : 0 ≤ liuPanPrimePowerCoprimeTotal N y q

The principal-character mass is nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerTotal_nonneg (N y : ℕ) : 0 ≤ liuPanPrimePowerTotal N y

The unrestricted coefficient mass is nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerTotal_eq_correctionBound_mod_one (N : ℕ) : liuPanPrimePowerTotal N N = liuPanSignedCorrectionBound N N 1 0 (liuWeight N (liuSourceZ10 N) (liuSourceY3 N))

The full coefficient mass is exactly the modulus-one correction.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerTotal_le_pairSqrtMass {C : ℝ} (hglobal : ∀ (t : ℕ), globalPrimePowerCorrection t ≤ C * √↑t) (N : ℕ) : liuPanPrimePowerTotal N N ≤ C * liuPanPrimePowerPairSqrtMass N

Chebyshev's global correction bound controls the full coefficient mass by the exact square-root mass of Liu's source pairs.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPairSqrtMass_nonneg (N : ℕ) : 0 ≤ liuPanPrimePowerPairSqrtMass N

The source-pair square-root mass is nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightPairs_source_card_le (N : ℕ) : (liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N)).card ≤ (⌊↑N ^ (1 / 3)⌋₊ + 1) * (⌊↑N ^ (9 / 20)⌋₊ + 1)

The exact source pair set injects into the rectangle supplied by Liu's p₁ ≤ N^(1/3) and corrected p₂ ≤ N^(9/20) cutoffs.

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightPairs_source_card_cast_le (N : ℕ) (hN : 1 ≤ N) : ↑(liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N)).card ≤ 4 * ↑N ^ (47 / 60)

A real-power form of the finite source-pair cardinality bound.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPairSqrtMass_le_rpow (N : ℕ) (hN : 8 ≤ N) : liuPanPrimePowerPairSqrtMass N ≤ 2 * √(liuWeightP₁ReciprocalBound * liuSourceR1P₂ReciprocalBound) * ↑N ^ (107 / 120)

Cauchy--Schwarz, the exact source rectangle, and the two uniform reciprocal prime sums put the source-pair square-root mass on the N^(107/120) scale.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoprimeTotal_le_total (N y q : ℕ) : liuPanPrimePowerCoprimeTotal N y q ≤ liuPanPrimePowerTotal N y

Restricting to units can only decrease the nonnegative coefficient mass.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoprimeTotal_mono {N y x q : ℕ} (hyx : y ≤ x) : liuPanPrimePowerCoprimeTotal N y q ≤ liuPanPrimePowerCoprimeTotal N x q

The coprime principal mass is monotone in the partial-sum cutoff.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerAPSum_eq_density_add_discrepancy {N y q l : ℕ} (hq : 0 < q) (hl : IsUnit ↑l) : liuPanPrimePowerAPSum N y q l = liuPanPrimePowerTotal N y / ↑q.totient + liuPanPrimePowerDiscrepancy N y q l

Exact principal-density plus discrepancy decomposition of the coefficient AP partial sum.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerAPSum_eq_coprimeDensity_add_nonprincipal (N y q l : ℕ) : liuPanPrimePowerAPSum N y q l = liuPanPrimePowerCoprimeTotal N y q / ↑q.totient + liuPanPrimePowerNonprincipalDiscrepancy N y q l

Exact principal-character density plus genuine nonprincipal discrepancy.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalDiscrepancy_eq_discrepancy_add_noncoprime {N y q l : ℕ} (hq : 0 < q) (hl : IsUnit ↑l) : liuPanPrimePowerNonprincipalDiscrepancy N y q l = liuPanPrimePowerDiscrepancy N y q l + liuPanPrimePowerNoncoprimeTotal N y q / ↑q.totient

The previous all-total discrepancy differs from the genuine nonprincipal discrepancy by exactly the omitted noncoprime principal-character mass.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSignedCorrectionBound_eq_density_add_discrepancy {N y q l : ℕ} (hy : y ≤ N) (hq : 0 < q) (hl : IsUnit ↑l) : liuPanSignedCorrectionBound y N q l (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) = liuPanPrimePowerTotal N y / ↑q.totient + liuPanPrimePowerDiscrepancy N y q l

Character reduction of Liu's correction bound at each nonzero unit progression. This combines the exact source regrouping with charSum_ap.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSignedCorrectionBound_eq_coprimeDensity_add_nonprincipal {N y q l : ℕ} (hy : y ≤ N) (hl : IsUnit ↑l) : liuPanSignedCorrectionBound y N q l (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) = liuPanPrimePowerCoprimeTotal N y q / ↑q.totient + liuPanPrimePowerNonprincipalDiscrepancy N y q l

Character reduction with the actual principal-character mass.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerDiscrepancy_mod_one (N y l : ℕ) : liuPanPrimePowerDiscrepancy N y 1 l = 0

At modulus one the character discrepancy vanishes exactly.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalDiscrepancy_mod_one (N y l : ℕ) : liuPanPrimePowerNonprincipalDiscrepancy N y 1 l = 0

At modulus one the genuine nonprincipal discrepancy also vanishes exactly.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight (q : ℕ) : ℝ

Liu's nonnegative squarefree modulus weight.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight q = ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight_zero : liuPanPrimePowerModulusWeight 0 = 0

The zero modulus is killed before any character argument is invoked.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight_nonneg (q : ℕ) : 0 ≤ liuPanPrimePowerModulusWeight q

Nonnegativity of the modulus weight used in the density and residual averages.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight_eq_zero_of_not_squarefree {q : ℕ} (hq : ¬Squarefree q) : liuPanPrimePowerModulusWeight q = 0

Nonsquarefree moduli have zero weight.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight_div_totient_mul_of_coprime {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) (hmn : m.Coprime n) : liuPanPrimePowerModulusWeight (m * n) / ↑(m * n).totient = liuPanPrimePowerModulusWeight m / ↑m.totient * (liuPanPrimePowerModulusWeight n / ↑n.totient)

The squarefree modulus weight divided by Euler's totient is multiplicative on positive coprime arguments.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight_div_totient_eq_three_factors {d r e : ℕ} (hsq : Squarefree (d * r)) (he : e ∣ r) : liuPanPrimePowerModulusWeight (d * r) / ↑(d * r).totient = liuPanPrimePowerModulusWeight d / ↑d.totient * (liuPanPrimePowerModulusWeight e / ↑e.totient) * (liuPanPrimePowerModulusWeight (r / e) / ↑(r / e).totient)

If d * r is squarefree and e ∣ r, its normalized modulus weight factors into the conductor, selected divisor, and complementary cofactor.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerH3Mass (Q : ℕ) : ℝ

The finite H₃ mass used when the squarefree modulus sum is regrouped conductor first.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerH3Mass Q = ∑ q ∈ Finset.range (Q + 1), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight q / ↑q.totient

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerJ9Mass (Q : ℕ) : ℝ

The finite J₉ mass generated by Cauchy--Schwarz in the squarefree cofactor variable.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerJ9Mass Q = ∑ d ∈ Finset.range (Q + 1), ↑(ArithmeticFunction.moebius d) ^ 2 * 9 ^ d.primeFactors.card / ↑d

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCofactorSqrtMass (Q : ℕ) : ℝ

The dilated-coefficient cofactor mass with the square-root saving supplied by the large sieve.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCofactorSqrtMass Q = ∑ e ∈ Finset.range (Q + 1), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight e / ↑e.totient / √↑e

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCofactorLinearMass (Q : ℕ) : ℝ

The stronger cofactor mass occurring in the Q² part of the large-sieve bound.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCofactorLinearMass Q = ∑ e ∈ Finset.range (Q + 1), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight e / ↑e.totient / ↑e

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerH3Mass_nonneg (Q : ℕ) : 0 ≤ liuPanPrimePowerH3Mass Q

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerJ9Mass_nonneg (Q : ℕ) : 0 ≤ liuPanPrimePowerJ9Mass Q

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerJ9_term_squarefree (d : ℕ) (hd : Squarefree d) : ↑(ArithmeticFunction.moebius d) ^ 2 * 9 ^ d.primeFactors.card / ↑d = ∏ p ∈ d.primeFactors, 9 / ↑p

On squarefree integers the J₉ summand is its expected Euler product.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerJ9_term_non_squarefree (d : ℕ) (hd : ¬Squarefree d) : ↑(ArithmeticFunction.moebius d) ^ 2 * 9 ^ d.primeFactors.card / ↑d = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerJ9Mass_le_prod_one_add (Q : ℕ) : liuPanPrimePowerJ9Mass Q ≤ ∏ p ∈ AnalyticNumberTheory.Mertens.primesUpTo Q, (1 + 9 / ↑p)

Subset expansion bounds the finite J₉ mass by its positive Euler product.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCofactorSqrtMass_nonneg (Q : ℕ) : 0 ≤ liuPanPrimePowerCofactorSqrtMass Q

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCofactorLinearMass_nonneg (Q : ℕ) : 0 ≤ liuPanPrimePowerCofactorLinearMass Q

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerH3Mass_eq_panMainTotientWeightedSum (Q : ℕ) : liuPanPrimePowerH3Mass Q = AnalyticNumberTheory.Sieve.panMainTotientWeightedSum Q

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCofactorSqrtMass_le_H3Mass (Q : ℕ) : liuPanPrimePowerCofactorSqrtMass Q ≤ liuPanPrimePowerH3Mass Q

The square-root cofactor mass is already dominated by H₃; no extra power of the conductor cutoff is lost.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCofactorLinearMass_le_H3Mass (Q : ℕ) : liuPanPrimePowerCofactorLinearMass Q ≤ liuPanPrimePowerH3Mass Q

The linearly damped cofactor mass is also dominated by H₃.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerH3Mass_le_polylog : ∃ (C : ℝ), 0 < C ∧ ∀ (Q : ℕ), liuPanPrimePowerH3Mass Q ≤ C * Real.log (↑Q + 2) ^ 6

The existing Pan main-term estimate is exactly the needed finite H₃ polylogarithmic bound.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerJ9Mass_le_polylog : ∃ (C : ℝ), 0 < C ∧ ∀ (Q : ℕ), liuPanPrimePowerJ9Mass Q ≤ C * Real.log (↑Q + 2) ^ 9

The second squarefree cofactor moment has the log⁹ growth predicted by its Euler product.

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

The density modulus mass occurring after averaging over Liu's moduli.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerDensityModulusMass N B = ∑ q ∈ Finset.range (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B + 1), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight q / ↑q.totient

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerDensityModulusMass_nonneg (N : ℕ) (B : ℝ) : 0 ≤ liuPanPrimePowerDensityModulusMass N B

The density modulus mass is nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerDensityModulusMass_eq_panMainTotientWeightedSum (N : ℕ) (B : ℝ) : liuPanPrimePowerDensityModulusMass N B = AnalyticNumberTheory.Sieve.panMainTotientWeightedSum (panModulusCutoff N B)

The density modulus mass is exactly the existing Pan main-term totient-weighted sum at Liu's modulus cutoff.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerDensityModulusMass_le_polylog : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ) (B : ℝ), liuPanPrimePowerDensityModulusMass N B ≤ C * Real.log (↑(panModulusCutoff N B) + 2) ^ 6

The known Pan modulus estimate supplies the required polylogarithmic density bound without discarding the arithmetic-progression structure.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerTotal_le_rpow : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ), 8 ≤ N → liuPanPrimePowerTotal N N ≤ C * ↑N ^ (107 / 120)

The unrestricted coefficient mass has a uniform power saving. The exponent comes only from the exact source rectangle and global Chebyshev control.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerDensityProduct_le_rpow_polylog : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ) (B : ℝ), 8 ≤ N → liuPanPrimePowerTotal N N * liuPanPrimePowerDensityModulusMass N B ≤ C * ↑N ^ (107 / 120) * Real.log (↑(panModulusCutoff N B) + 2) ^ 6

The density product has the explicit power-saving coefficient scale, uniformly in the modulus cutoff.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerDiscrepancyMaxL (N y q : ℕ) : ℝ

The maximal character discrepancy over unit residue classes.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerDiscrepancyMaxL N y q = if h : (AnalyticNumberTheory.Sieve.unitResidues q).Nonempty then (Finset.image (fun (l : ℕ) => |MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerDiscrepancy N y q l|) (AnalyticNumberTheory.Sieve.unitResidues q)).max' ⋯ else 0

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

The maximal character discrepancy over y ≤ N and unit residues.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerDiscrepancyMaxY N q = (Finset.image (fun (y : ℕ) => MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerDiscrepancyMaxL N y q) (Finset.range (N + 1))).max' ⋯

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

A transparent weighted maximal character residual, with no large-sieve estimate asserted.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainPanPrimePowerCharacterResidual N B = ∑ q ∈ Finset.range (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B + 1), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight q * MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerDiscrepancyMaxY N q

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalDiscrepancyMaxL (N y q : ℕ) : ℝ

The maximal genuine nonprincipal discrepancy over unit residue classes.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalDiscrepancyMaxL N y q = if h : (AnalyticNumberTheory.Sieve.unitResidues q).Nonempty then (Finset.image (fun (l : ℕ) => |MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalDiscrepancy N y q l|) (AnalyticNumberTheory.Sieve.unitResidues q)).max' ⋯ else 0

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

The maximal genuine nonprincipal discrepancy over y ≤ N and unit residue classes.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalDiscrepancyMaxY N q = (Finset.image (fun (y : ℕ) => MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalDiscrepancyMaxL N y q) (Finset.range (N + 1))).max' ⋯

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

The transparent residual after the true principal mass is removed. Via liuPanPrimePowerNonprincipalDiscrepancy_eq_discrepancy_add_noncoprime, it is exactly the old character discrepancy together with its noncoprime correction.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainPanPrimePowerCharacterNoncoprimeResidual N B = ∑ q ∈ Finset.range (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B + 1), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight q * MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalDiscrepancyMaxY N q

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerTotal_mono {N y x : ℕ} (hyx : y ≤ x) : liuPanPrimePowerTotal N y ≤ liuPanPrimePowerTotal N x

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerDiscrepancy_le_maxY {N y q l : ℕ} (hy : y ≤ N) (hl : l ∈ AnalyticNumberTheory.Sieve.unitResidues q) : liuPanPrimePowerDiscrepancy N y q l ≤ liuPanPrimePowerDiscrepancyMaxY N q

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalDiscrepancy_le_maxY {N y q l : ℕ} (hy : y ≤ N) (hl : l ∈ AnalyticNumberTheory.Sieve.unitResidues q) : liuPanPrimePowerNonprincipalDiscrepancy N y q l ≤ liuPanPrimePowerNonprincipalDiscrepancyMaxY N q

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAPPrimePowerCorrectionMaxY_le_coprimeDensity_add_nonprincipal (N q : ℕ) (hq : 0 < q) : liuPanAPPrimePowerCorrectionMaxY N q N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) ≤ liuPanPrimePowerCoprimeTotal N N q / ↑q.totient + liuPanPrimePowerNonprincipalDiscrepancyMaxY N q

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAPPrimePowerCorrectionMaxY_le_density_add_character (N q : ℕ) (hq : 0 < q) : liuPanAPPrimePowerCorrectionMaxY N q N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) ≤ liuPanPrimePowerTotal N N / ↑q.totient + liuPanPrimePowerDiscrepancyMaxY N q

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanAPPrimePowerCorrectionAverage_le_density_add_character (N : ℕ) (B : ℝ) : ∑ q ∈ Finset.range (panModulusCutoff N B + 1), liuPanPrimePowerModulusWeight q * liuPanAPPrimePowerCorrectionMaxY N q N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) ≤ liuPanPrimePowerTotal N N * liuPanPrimePowerDensityModulusMass N B + liuMainPanPrimePowerCharacterResidual N B

Exact structural reduction of the prime-power average: a coefficient mass times the totient-weighted modulus density, plus one maximal character residual. No estimate for the residual is asserted here.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanAPPrimePowerCorrectionAverage_le_density_add_characterNoncoprime (N : ℕ) (B : ℝ) : ∑ q ∈ Finset.range (panModulusCutoff N B + 1), liuPanPrimePowerModulusWeight q * liuPanAPPrimePowerCorrectionMaxY N q N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) ≤ liuPanPrimePowerTotal N N * liuPanPrimePowerDensityModulusMass N B + liuMainPanPrimePowerCharacterNoncoprimeResidual N B

Source-faithful reduction of the averaged correction: the true coprime principal mass is bounded by the full coefficient mass, while all remaining character and noncoprime effects stay in one explicit maximal residual.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanAPPrimePowerCorrectionAverage_le_polylog_add_characterNoncoprime : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ) (B : ℝ), ∑ q ∈ Finset.range (panModulusCutoff N B + 1), liuPanPrimePowerModulusWeight q * liuPanAPPrimePowerCorrectionMaxY N q N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) ≤ liuPanPrimePowerTotal N N * (C * Real.log (↑(panModulusCutoff N B) + 2) ^ 6) + liuMainPanPrimePowerCharacterNoncoprimeResidual N B

The density term in the averaged correction is bounded by the known polylogarithmic modulus sum; no estimate for the explicit residual is asserted.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanAPPrimePowerCorrectionAverage_le_rpow_polylog_add_characterNoncoprime : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ) (B : ℝ), 8 ≤ N → ∑ q ∈ Finset.range (panModulusCutoff N B + 1), liuPanPrimePowerModulusWeight q * liuPanAPPrimePowerCorrectionMaxY N q N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) ≤ C * ↑N ^ (107 / 120) * Real.log (↑(panModulusCutoff N B) + 2) ^ 6 + liuMainPanPrimePowerCharacterNoncoprimeResidual N B

Quantitative density reduction of Liu's exact AP correction average. The only unestimated term is the displayed maximal character/noncoprime residual.