Combined inverse-log discrepancy for Liu's Pan endpoint

The Type I endpoint, Type II endpoint, and complete signed-main kernel are recombined before taking an absolute value. Vaughan's finite identity then identifies this expression with the source-weighted Λ / log discrepancy. The already separated prime-power correction remains on its own power-saving scale.

The older componentwise contracts are intentionally left unchanged. Their degenerate or conductor-one endpoint behavior does not prove the combined estimate introduced here.

Exact finite combination

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogDiscrepancy (main : ℝ → ℝ) (y X q l : ℕ) (f : ℕ → ℝ) (u v : ℕ) : ℝ

The Type I endpoint, Type II endpoint, and complete signed main, combined inside one absolute value before any analytic estimate is applied.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogDiscrepancy main y X q l f u v = |((AnalyticNumberTheory.Sieve.panPieceSum y X q l f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV1 y q l u / Real.log ↑y) + AnalyticNumberTheory.Sieve.panPieceSum y X q l f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV3 y q l u v / Real.log ↑y) + MathlibNt.SieveTheory.LiuWeight.liuPanSignedMainSum main y X q l f u v|

theorem MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogDiscrepancy_eq (main : ℝ → ℝ) (y X q l : ℕ) (f : ℕ → ℝ) (u v : ℕ) : liuPanCombinedInverseLogDiscrepancy main y X q l f u v = |∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * (AnalyticNumberTheory.Sieve.apLogVonMangoldt (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) - main (↑y / ↑a) / ↑q.totient) else 0|

Vaughan's logarithmic identity recombines the three endpoint terms into the exact source-weighted Λ / log discrepancy.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogDiscrepancy_source_eq (kappa : ℝ) (N y q l u v : ℕ) : liuPanCombinedInverseLogDiscrepancy (liuLogarithmicIntegral kappa) y N q l (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) u v = |∑ a ∈ Finset.Icc 1 N, if a.Coprime q then liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a * (AnalyticNumberTheory.Sieve.apLogVonMangoldt (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) - liuLogarithmicIntegral kappa (↑y / ↑a) / ↑q.totient) else 0|

Source-facing specialization of the exact combined identity.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogMaxL (main : ℝ → ℝ) (y X q : ℕ) (f : ℕ → ℝ) (u v : ℕ) : ℝ

Maximum of the exact combined discrepancy over canonical reduced residues.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogMaxL main y X q f u v = if h : (AnalyticNumberTheory.Sieve.unitResidues q).Nonempty then (Finset.image (fun (l : ℕ) => MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogDiscrepancy main y X q l f u v) (AnalyticNumberTheory.Sieve.unitResidues q)).max' ⋯ else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogMaxY (main : ℝ → ℝ) (X q x : ℕ) (f : ℕ → ℝ) (u v : ℕ) : ℝ

Maximum of the exact combined discrepancy over y ≤ x.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogMaxY main X q x f u v = (Finset.image (fun (y : ℕ) => MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogMaxL main y X q f u v) (Finset.range (x + 1))).max' ⋯

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogMaxL_zero (main : ℝ → ℝ) (y X : ℕ) (f : ℕ → ℝ) (u v : ℕ) : liuPanCombinedInverseLogMaxL main y X 0 f u v = 0

The zero modulus has no canonical reduced residue.

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogMaxL_one (main : ℝ → ℝ) (y X : ℕ) (f : ℕ → ℝ) (u v : ℕ) : liuPanCombinedInverseLogMaxL main y X 1 f u v = liuPanCombinedInverseLogDiscrepancy main y X 1 0 f u v

Modulus one uses its unique canonical residue 0.

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogMaxY_zero (main : ℝ → ℝ) (X x : ℕ) (f : ℕ → ℝ) (u v : ℕ) : liuPanCombinedInverseLogMaxY main X 0 x f u v = 0

The zero-modulus y-maximum is canonically zero.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogMaxY_one (main : ℝ → ℝ) (X x : ℕ) (f : ℕ → ℝ) (u v : ℕ) : liuPanCombinedInverseLogMaxY main X 1 x f u v = (Finset.image (fun (y : ℕ) => liuPanCombinedInverseLogDiscrepancy main y X 1 0 f u v) (Finset.range (x + 1))).max' ⋯

The modulus-one y-maximum retains the unique residue 0.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogDiscrepancy_nonneg (main : ℝ → ℝ) (y X q l : ℕ) (f : ℕ → ℝ) (u v : ℕ) : 0 ≤ liuPanCombinedInverseLogDiscrepancy main y X q l f u v

theorem MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogMaxL_nonneg (main : ℝ → ℝ) (y X q : ℕ) (f : ℕ → ℝ) (u v : ℕ) : 0 ≤ liuPanCombinedInverseLogMaxL main y X q f u v

theorem MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogMaxY_nonneg (main : ℝ → ℝ) (X q x : ℕ) (f : ℕ → ℝ) (u v : ℕ) : 0 ≤ liuPanCombinedInverseLogMaxY main X q x f u v

Exact correction separation and maxima

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuMainPanCoprimeSum_le_combinedInverseLog_add_primePower (main : ℝ → ℝ) (y X q l : ℕ) (f : ℕ → ℝ) (u v : ℕ) (hf0 : f 0 = 0) : |liuMainPanCoprimeSum main y X q l f| ≤ liuPanCombinedInverseLogDiscrepancy main y X q l f u v + liuPanSignedCorrectionBound y X q l f

Only the prime-power correction is separated after the three principal endpoint terms have been recombined.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanMaxL_le_combinedInverseLog_add_primePower (main : ℝ → ℝ) (y X q : ℕ) (f : ℕ → ℝ) (u v : ℕ) (hf0 : f 0 = 0) : liuMainPanMaxL main y X q f ≤ liuPanCombinedInverseLogMaxL main y X q f u v + liuPanAPPrimePowerCorrectionMaxL y X q f

The canonical residue maximum inherits the exact combined-plus-correction bound.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanMaxY_le_combinedInverseLog_add_primePower (main : ℝ → ℝ) (X q x : ℕ) (f : ℕ → ℝ) (u v : ℕ) (hf0 : f 0 = 0) : liuMainPanMaxY main X q x f ≤ liuPanCombinedInverseLogMaxY main X q x f u v + liuPanAPPrimePowerCorrectionMaxY X q x f

The two nested maxima preserve the combined-before-absolute-value route.

Source-family analytic input

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuMainPanCombinedInverseLogAverage (kappa : ℝ) (N : ℕ) (B : ℝ) (u v : ℕ) : ℝ

The weighted combined inverse-log average for Liu's source at a fixed N.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainPanCombinedInverseLogAverage kappa N B u v = ∑ q ∈ Finset.range (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogMaxY (MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral kappa) N q N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) u v

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanCombinedInverseLogBoundAt (kappa : ℝ) (N : ℕ) (A B C : ℝ) (u v : ℕ) : Prop

The fixed-source combined inverse-log estimate.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanCombinedInverseLogBoundAt kappa N A B C u v = (MathlibNt.SieveTheory.LiuWeight.liuMainPanCombinedInverseLogAverage kappa N B u v ≤ C * ↑N / Real.log ↑N ^ A)

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanCombinedInverseLogSourceFamilyBound (kappa : ℝ) (u v : ℕ) : Prop

The source-family combined estimate, with f_N chosen inside the final universal quantifier over N.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanCombinedInverseLogSourceFamilyBound kappa u v = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N0 : ℕ), ∀ (N : ℕ), N0 ≤ N → MathlibNt.SieveTheory.LiuWeight.LiuMainPanCombinedInverseLogBoundAt kappa N A B C u v

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanWeightedSum_le_combinedInverseLog_add_primePower (kappa : ℝ) (N : ℕ) (B : ℝ) (u v : ℕ) : liuMainPanWeightedSum (liuLogarithmicIntegral kappa) N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) B ≤ liuMainPanCombinedInverseLogAverage kappa N B u v + liuMainPanAPPrimePowerCorrectionAverage N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) B

The source Pan average is bounded by the combined discrepancy and only the separately controlled prime-power correction.

theorem MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceFullDistributionMajorant_le_of_combinedInverseLog (kappa epsilon A B C Cpp delta K : ℝ) (N u v : ℕ) (hN : 8 ≤ N) (hepsilon : 0 ≤ epsilon) (hcut : liuSourceDEpsilon N epsilon ≤ panModulusCutoff N B) (hcombined : LiuMainPanCombinedInverseLogBoundAt kappa N A B C u v) (hpp : LiuMainPanAPPrimePowerPowerSavingBoundAt N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) B Cpp delta K) : liuPaperQSourceFullDistributionMajorant (liuLogarithmicIntegral kappa) N epsilon ≤ C * ↑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 eqn-r consumer. The combined inverse-log estimate and the prime-power power saving remain on their distinct scales.

Source-family and little-oh consumers

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuPaperQSourceFullDistributionMajorant_le_of_combinedInverseLog (kappa epsilon : ℝ) (u v : ℕ) (hepsilon : 0 < epsilon) (hcombined : LiuMainPanCombinedInverseLogSourceFamilyBound kappa u v) : ∃ (C : ℝ), 0 < C ∧ ∃ (Cpp : ℝ), 0 < Cpp ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∀ᶠ (N : ℕ) in Filter.atTop, liuPaperQSourceFullDistributionMajorant (liuLogarithmicIntegral kappa) N epsilon ≤ C * ↑N / Real.log ↑N ^ 3 + Cpp * ↑N ^ (1 - 1 / 30) * Real.log ↑N ^ 20 + 15 * liuLogarithmicIntegralUpperConstant kappa * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2

The source-family combined estimate and the proved source prime-power endpoint give the exact eqn-r majorant with three distinct scales.

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_inverseLogCubeScale_div_mainScale (C : ℝ) : Filter.Tendsto (fun (N : ℕ) => C * ↑N / Real.log ↑N ^ 3 / (↑N / Real.log ↑N ^ 2)) Filter.atTop (nhds 0)

A cubic inverse-log bound is negligible relative to N / log(N)^2.

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_liuPaperQSourceFullDistributionMajorant_div_mainScale_of_combinedInverseLog (kappa epsilon : ℝ) (u v : ℕ) (hepsilon : 0 < epsilon) (hcombined : LiuMainPanCombinedInverseLogSourceFamilyBound kappa u v) : Filter.Tendsto (fun (N : ℕ) => liuPaperQSourceFullDistributionMajorant (liuLogarithmicIntegral kappa) N epsilon / (↑N / Real.log ↑N ^ 2)) Filter.atTop (nhds 0)

The exact Liu eqn-r distribution majorant is o(N / log(N)^2) under the combined source-family predicate. The proved prime-power power saving and the established R₁ estimate are used only at their own scales.

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_abs_liuSelbergRemainder_div_mainScale_of_combinedInverseLog (kappa epsilon : ℝ) (u v : ℕ) (lambda : ℕ → ℕ → ℝ) (hepsilon : 0 < epsilon) (hlambda : ∀ᶠ (N : ℕ) in Filter.atTop, LiuSelbergLambdaAdmissible N epsilon (lambda N)) (hcombined : LiuMainPanCombinedInverseLogSourceFamilyBound kappa u v) : Filter.Tendsto (fun (N : ℕ) => |liuSelbergRemainder (liuLogarithmicIntegral kappa) N epsilon (lambda N)| / (↑N / Real.log ↑N ^ 2)) Filter.atTop (nhds 0)

Consequently, every eventually admissible Selberg lambda family has its actual signed remainder negligible on the downstream main scale.