Liu's prime-power correction on its own power-saving scale

This module keeps the existing arbitrary-A signed-residual interfaces intact and adds the source-faithful alternative needed by Liu's argument. Type I, Type II, and the complete signed main retain the N / log(N)^A scale. The exact AP prime-power correction is a separate input on the N^(1 - delta) log(N)^K scale, and the established R₁ term remains separate.

The estimate demanded by LiuMainPanAPPrimePowerPowerSavingBoundAt is proved below for Liu's source weight, with the safe exponents delta = 1/30 and K = 20.

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

The exact weighted AP prime-power correction average at the source parameter N.

Equations

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

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanAPPrimePowerPowerSavingBoundAt (N : ℕ) (f : ℕ → ℝ) (B Cpp delta K : ℝ) : Prop

A transparent fixed-N power-saving input for the exact AP prime-power correction average. In particular, delta is required to be positive.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanAPPrimePowerPowerSavingBoundAt N f B Cpp delta K = (0 < delta ∧ MathlibNt.SieveTheory.LiuWeight.liuMainPanAPPrimePowerCorrectionAverage N f B ≤ Cpp * ↑N ^ (1 - delta) * Real.log ↑N ^ K)

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanPrimePowerPowerSavingInputsAt (distMain : ℝ → ℝ) (N : ℕ) (f : ℕ → ℝ) (A B C1 C2 Cmain Cpp delta K : ℝ) (u v : ℕ) : Prop

The four source-faithful finite inputs, with the prime-power correction kept on its own power-saving scale.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanPrimePowerPowerSavingInputsAt distMain N f A B C1 C2 Cmain Cpp delta K u v = (MathlibNt.SieveTheory.LiuWeight.LiuMainPanTypeIPieceBoundAt N f A B C1 u ∧ MathlibNt.SieveTheory.LiuWeight.LiuMainPanTypeIIPieceBoundAt N f A B C2 u v ∧ MathlibNt.SieveTheory.LiuWeight.LiuMainPanSignedMainBoundAt distMain N f A B Cmain u v ∧ MathlibNt.SieveTheory.LiuWeight.LiuMainPanAPPrimePowerPowerSavingBoundAt N f B Cpp delta K)

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanPrimePowerPowerSavingSourceFamilyInputs (distMain : ℝ → ℝ) (A B C1 C2 Cmain Cpp delta K : ℝ) (u v : ℕ) : Prop

Eventual source-family packaging of the four separate finite inputs.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanPrimePowerPowerSavingSourceFamilyInputs distMain A B C1 C2 Cmain Cpp delta K u v = ∀ᶠ (N : ℕ) in Filter.atTop, MathlibNt.SieveTheory.LiuWeight.LiuMainPanPrimePowerPowerSavingInputsAt distMain N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) A B C1 C2 Cmain Cpp delta K u v

theorem MathlibNt.SieveTheory.LiuWeight.exists_liuMainPanAPPrimePowerPowerSavingBoundAt_source (B : ℝ) (hB : 0 ≤ B) : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ), 8 ≤ N → LiuMainPanAPPrimePowerPowerSavingBoundAt N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) B C (1 / 30) 20

Liu's source prime-power correction satisfies a uniform finite power-saving bound for every nonnegative logarithmic conductor exponent.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuMainPanAPPrimePowerPowerSavingBoundAt_source (B : ℝ) (hB : 0 ≤ B) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop, LiuMainPanAPPrimePowerPowerSavingBoundAt N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) B C (1 / 30) 20

Eventual source-family form of the prime-power power saving.

theorem MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceCoprimeDistributionMajorant_le_liuMainPanAverage (main : ℝ → ℝ) (N : ℕ) (epsilon B : ℝ) (hN : 1 ≤ N) (hcut : liuSourceDEpsilon N epsilon ≤ panModulusCutoff N B) : liuPaperQSourceCoprimeDistributionMajorant main N epsilon ≤ ∑ q ∈ Finset.range (panModulusCutoff N B + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * liuMainPanMaxY main N q N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N))

The coprime source majorant is bounded by the raw fixed-N Pan average. This is the scale-neutral form of the existing structural consumption bridge.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanAverage_le_of_primePowerPowerSavingInputsAt (distMain : ℝ → ℝ) (N : ℕ) (f : ℕ → ℝ) (A B C1 C2 Cmain Cpp delta K : ℝ) (u v : ℕ) (hf0 : f 0 = 0) (hsource : LiuMainPanPrimePowerPowerSavingInputsAt distMain N f A B C1 C2 Cmain Cpp delta K u v) : ∑ q ∈ Finset.range (panModulusCutoff N B + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * liuMainPanMaxY distMain N q N f ≤ (C1 + C2 + Cmain) * ↑N / Real.log ↑N ^ A + Cpp * ↑N ^ (1 - delta) * Real.log ↑N ^ K

The four finite inputs bound the raw Pan average, with the prime-power term displayed separately and without absorption.

theorem MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceFullDistributionMajorant_liuLogarithmicIntegral_le_of_primePowerPowerSavingInputsAt (kappa epsilon A B C1 C2 Cmain Cpp delta K : ℝ) (N u v : ℕ) (hN : 8 ≤ N) (hepsilon : 0 ≤ epsilon) (hcut : liuSourceDEpsilon N epsilon ≤ panModulusCutoff N B) (hsource : LiuMainPanPrimePowerPowerSavingInputsAt (liuLogarithmicIntegral kappa) N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B C1 C2 Cmain Cpp delta K u v) : liuPaperQSourceFullDistributionMajorant (liuLogarithmicIntegral kappa) N epsilon ≤ (C1 + C2 + Cmain) * ↑N / Real.log ↑N ^ A + Cpp * ↑N ^ (1 - delta) * Real.log ↑N ^ K + 15 * liuLogarithmicIntegralUpperConstant kappa * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2

Fixed-N assembly into Liu's full source distribution majorant. The arbitrary-A terms, prime-power term, and R₁ term remain separate.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuPaperQSourceFullDistributionMajorant_liuLogarithmicIntegral_le_of_primePowerPowerSavingInputs (kappa epsilon A B C1 C2 Cmain Cpp delta K : ℝ) (u v : ℕ) (hepsilon : 0 < epsilon) (hB : 0 ≤ B) (hsource : LiuMainPanPrimePowerPowerSavingSourceFamilyInputs (liuLogarithmicIntegral kappa) A B C1 C2 Cmain Cpp delta K u v) : ∀ᶠ (N : ℕ) in Filter.atTop, liuPaperQSourceFullDistributionMajorant (liuLogarithmicIntegral kappa) N epsilon ≤ (C1 + C2 + Cmain) * ↑N / Real.log ↑N ^ A + Cpp * ↑N ^ (1 - delta) * Real.log ↑N ^ K + 15 * liuLogarithmicIntegralUpperConstant kappa * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2

Eventual assembly into the full source distribution majorant.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuSelbergRemainder_liuLogarithmicIntegral_le_of_primePowerPowerSavingInputsAt (kappa epsilon A B C1 C2 Cmain Cpp delta K : ℝ) (N u v : ℕ) (lambda : ℕ → ℝ) (hN : 8 ≤ N) (hepsilon : 0 ≤ epsilon) (hcut : liuSourceDEpsilon N epsilon ≤ panModulusCutoff N B) (hlambda : LiuSelbergLambdaAdmissible N epsilon lambda) (hsource : LiuMainPanPrimePowerPowerSavingInputsAt (liuLogarithmicIntegral kappa) N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B C1 C2 Cmain Cpp delta K u v) : |liuSelbergRemainder (liuLogarithmicIntegral kappa) N epsilon lambda| ≤ (C1 + C2 + Cmain) * ↑N / Real.log ↑N ^ A + Cpp * ↑N ^ (1 - delta) * Real.log ↑N ^ K + 15 * liuLogarithmicIntegralUpperConstant kappa * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2

Fixed-N assembly for the actual signed lambda-pair Selberg remainder.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_abs_liuSelbergRemainder_liuLogarithmicIntegral_le_of_primePowerPowerSavingInputs (kappa epsilon A B C1 C2 Cmain Cpp delta K : ℝ) (u v : ℕ) (lambda : ℕ → ℕ → ℝ) (hepsilon : 0 < epsilon) (hB : 0 ≤ B) (hlambda : ∀ᶠ (N : ℕ) in Filter.atTop, LiuSelbergLambdaAdmissible N epsilon (lambda N)) (hsource : LiuMainPanPrimePowerPowerSavingSourceFamilyInputs (liuLogarithmicIntegral kappa) A B C1 C2 Cmain Cpp delta K u v) : ∀ᶠ (N : ℕ) in Filter.atTop, |liuSelbergRemainder (liuLogarithmicIntegral kappa) N epsilon (lambda N)| ≤ (C1 + C2 + Cmain) * ↑N / Real.log ↑N ^ A + Cpp * ↑N ^ (1 - delta) * Real.log ↑N ^ K + 15 * liuLogarithmicIntegralUpperConstant kappa * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2

Eventual assembly for the actual signed lambda-pair Selberg remainder.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergSwitchedCount_le_of_mainTermUpperBound_primePowerPowerSavingInputsAt (kappa epsilon A B C1 C2 Cmain Cpp delta K : ℝ) (N u v : ℕ) (lambda : ℕ → ℝ) (hN : 8 ≤ N) (hepsilon : 0 ≤ epsilon) (hcut : liuSourceDEpsilon N epsilon ≤ panModulusCutoff N B) (hmainTerm : LiuSelbergMainTermUpperBound kappa N epsilon lambda) (hlambda : LiuSelbergLambdaAdmissible N epsilon lambda) (hsource : LiuMainPanPrimePowerPowerSavingInputsAt (liuLogarithmicIntegral kappa) N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B C1 C2 Cmain Cpp delta K u v) : liuSelbergSwitchedCount N epsilon lambda ≤ 3.94033 * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 + ((C1 + C2 + Cmain) * ↑N / Real.log ↑N ^ A + Cpp * ↑N ^ (1 - delta) * Real.log ↑N ^ K + 15 * liuLogarithmicIntegralUpperConstant kappa * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2)

Fixed-N switched-count assembly, conditional on the displayed numerical main-term input.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuSelbergSwitchedCount_le_of_mainTermUpperBound_primePowerPowerSavingInputs (kappa epsilon A B C1 C2 Cmain Cpp delta K : ℝ) (u v : ℕ) (lambda : ℕ → ℕ → ℝ) (hepsilon : 0 < epsilon) (hB : 0 ≤ B) (hmainTerm : ∀ᶠ (N : ℕ) in Filter.atTop, LiuSelbergMainTermUpperBound kappa N epsilon (lambda N)) (hlambda : ∀ᶠ (N : ℕ) in Filter.atTop, LiuSelbergLambdaAdmissible N epsilon (lambda N)) (hsource : LiuMainPanPrimePowerPowerSavingSourceFamilyInputs (liuLogarithmicIntegral kappa) A B C1 C2 Cmain Cpp delta K u v) : ∀ᶠ (N : ℕ) in Filter.atTop, liuSelbergSwitchedCount N epsilon (lambda N) ≤ 3.94033 * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 + ((C1 + C2 + Cmain) * ↑N / Real.log ↑N ^ A + Cpp * ↑N ^ (1 - delta) * Real.log ↑N ^ K + 15 * liuLogarithmicIntegralUpperConstant kappa * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2)

Eventual switched-count assembly for an arbitrary admissible lambda family.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuSelbergOptimalSquareCount_le_even_of_primePowerPowerSavingInputs (kappa epsilon A B C1 C2 Cmain Cpp delta K : ℝ) (u v : ℕ) (hkappa : 0 ≤ kappa) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hB : 0 ≤ B) (hsource : LiuMainPanPrimePowerPowerSavingSourceFamilyInputs (liuLogarithmicIntegral kappa) A B C1 C2 Cmain Cpp delta K u v) : ∀ᶠ (N : ℕ) in Filter.atTop ⊓ Filter.principal {N : ℕ | Even N}, liuSelbergSquareCount N epsilon (liuSelbergOptimalLambda N epsilon) ≤ 3.94033 * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 + ((C1 + C2 + Cmain) * ↑N / Real.log ↑N ^ A + Cpp * ↑N ^ (1 - delta) * Real.log ↑N ^ K + 15 * liuLogarithmicIntegralUpperConstant kappa * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2)

The optimal even-filter square count with all three error scales displayed.

Symbolic asymptotic consumers

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_primePowerPowerSavingScale_div_mainScale (delta K : ℝ) (hdelta : 0 < delta) : Filter.Tendsto (fun (N : ℕ) => ↑N ^ (1 - delta) * Real.log ↑N ^ K / (↑N / Real.log ↑N ^ 2)) Filter.atTop (nhds 0)

For every fixed positive delta and real logarithmic exponent K, the prime-power scale is negligible relative to N / log(N)^2.

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_liuR1Scale_div_mainScale : Filter.Tendsto (fun (N : ℕ) => ↑N ^ (9 / 10) * Real.log ↑N ^ 2 / (↑N / Real.log ↑N ^ 2)) Filter.atTop (nhds 0)

The unchanged N^(9/10) log(N)^2 scale from R₁ is also negligible relative to N / log(N)^2; this is kept as a separate triangular consumer.

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_primePower_add_liuR1_div_mainScale (Cpp CR1 delta K : ℝ) (hdelta : 0 < delta) : Filter.Tendsto (fun (N : ℕ) => (Cpp * (↑N ^ (1 - delta) * Real.log ↑N ^ K) + CR1 * (↑N ^ (9 / 10) * Real.log ↑N ^ 2)) / (↑N / Real.log ↑N ^ 2)) Filter.atTop (nhds 0)

Constant multiples of the separate prime-power and R₁ scales remain negligible when combined only after their individual estimates.