Exact Abel reduction for Liu's combined inverse-log discrepancy

This file applies finite summation by parts to the complete arithmetic-progression von Mangoldt sum. Its main route forms the source aggregate before taking an absolute value: quotient shells and prefix swaps are exact finite identities. The older sourcewise triangle route is retained below only as a diagnostic. It is analytically too strong because the empty-progression tail with q > y / a survives after taking absolute values source by source.

Complete AP psi sums and finite Abel summation

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

The complete von Mangoldt sum in one arithmetic progression, including the harmless indices 0 and 1.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAPPsi y q l = ∑ n ∈ Finset.range (y + 1), if n ≡ l [MOD q] then ArithmeticFunction.vonMangoldt n else 0

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

The complete AP psi discrepancy from the uniform main term y / phi(q).

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAPPsiDiscrepancy y q l = MathlibNt.SieveTheory.LiuWeight.liuPanAPPsi y q l - ↑y / ↑q.totient

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

The finite Abel weight for 1 / log. It is explicitly zero at 0 and 1.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanInverseLogAbelWeight n = if 2 ≤ n then (Real.log ↑n)⁻¹ - (Real.log ↑(n + 1))⁻¹ else 0

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

The discrete main term obtained by applying the same Abel transform to x.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanDiscreteInverseLogMain y = (Real.log ↑y)⁻¹ * ↑y + ∑ n ∈ Finset.range y, MathlibNt.SieveTheory.LiuWeight.liuPanInverseLogAbelWeight n * ↑n

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAPPsi_zero (q l : ℕ) : liuPanAPPsi 0 q l = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAPPsi_one (q l : ℕ) : liuPanAPPsi 1 q l = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanInverseLogAbelWeight_zero : liuPanInverseLogAbelWeight 0 = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanInverseLogAbelWeight_one : liuPanInverseLogAbelWeight 1 = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuPanInverseLogAbelWeight_nonneg (n : ℕ) : 0 ≤ liuPanInverseLogAbelWeight n

theorem MathlibNt.SieveTheory.LiuWeight.apLogVonMangoldt_eq_discreteAbel (y q l : ℕ) : AnalyticNumberTheory.Sieve.apLogVonMangoldt y q l = (Real.log ↑y)⁻¹ * liuPanAPPsi y q l + ∑ n ∈ Finset.range y, liuPanInverseLogAbelWeight n * liuPanAPPsi n q l

Exact finite discrete Abel summation for the AP sum of Λ(n) / log n. The exceptional terms n = 0, 1 vanish before a logarithmic denominator is used, and the displayed prefix weights are nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.apLogVonMangoldt_sub_liuLogarithmicIntegral_eq_discreteAbel (kappa : ℝ) (y : ℕ) (x : ℝ) (q l : ℕ) : AnalyticNumberTheory.Sieve.apLogVonMangoldt y q l - liuLogarithmicIntegral kappa x / ↑q.totient = (Real.log ↑y)⁻¹ * liuPanAPPsiDiscrepancy y q l + ∑ n ∈ Finset.range y, liuPanInverseLogAbelWeight n * liuPanAPPsiDiscrepancy n q l + (liuPanDiscreteInverseLogMain y - liuLogarithmicIntegral kappa x) / ↑q.totient

Exact decomposition of the inverse-log discrepancy into the endpoint psi discrepancy, all preceding psi discrepancies, and the deterministic discrete main-term error. This identity is valid for every modulus, including 0 and 1.

Aggregate-before-absolute-value Abel identities

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateAPPsiDiscrepancy (t A q l : ℕ) (f : ℕ → ℝ) : ℝ

The source-aggregated AP psi discrepancy up to A. The residue attached to a source index a is the canonical representative of a⁻¹ l (mod q).

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateAPPsiDiscrepancy t A q l f = ∑ a ∈ Finset.Icc 1 A, if a.Coprime q then f a * MathlibNt.SieveTheory.LiuWeight.liuPanAPPsiDiscrepancy t q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) else 0

def MathlibNt.SieveTheory.LiuWeight.liuPanAbelSourceCutoff (y X k : ℕ) : ℕ

The source cutoff in the quotient shell indexed by k. The value at zero is deliberately the full source endpoint.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAbelSourceCutoff y X k = if k = 0 then X else min X (y / k)

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAbelSourceCutoff_zero (y X : ℕ) : liuPanAbelSourceCutoff y X 0 = X

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAbelSourceCutoff_of_pos (y X k : ℕ) (hk : 0 < k) : liuPanAbelSourceCutoff y X k = min X (y / k)

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAbelSourceCutoff_succ (y X k : ℕ) : liuPanAbelSourceCutoff y X (k + 1) = min X (y / (k + 1))

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAbelSourceCutoff_le (y X k : ℕ) : liuPanAbelSourceCutoff y X k ≤ X

theorem MathlibNt.SieveTheory.LiuWeight.le_liuPanAbelSourceCutoff_iff (y X a k : ℕ) (hk : 0 < k) (haX : a ≤ X) (ha : 0 < a) : a ≤ liuPanAbelSourceCutoff y X k ↔ k ≤ y / a

theorem MathlibNt.SieveTheory.LiuWeight.sum_source_eq_sum_quotient_shells {R : Type u_1} [CommRing R] (y X : ℕ) (g : ℕ → R) (F : ℕ → ℕ → R) (hg0 : g 0 = 0) : ∑ a ∈ Finset.Icc 1 X, g (y / a) * F (y / a) a = ∑ k ∈ Finset.Icc 1 y, g k * (∑ a ∈ Finset.Icc 1 (liuPanAbelSourceCutoff y X k), F k a - ∑ a ∈ Finset.Icc 1 (liuPanAbelSourceCutoff y X (k + 1)), F k a)

Quotient fibers are exactly the successive source-cutoff shells. The assumption g 0 = 0 disposes of the sources with y / a = 0 exactly.

theorem MathlibNt.SieveTheory.LiuWeight.sum_source_prefix_eq_sum_aggregate_prefix {R : Type u_1} [CommRing R] (y X : ℕ) (w : ℕ → R) (F : ℕ → ℕ → R) : ∑ a ∈ Finset.Icc 1 X, ∑ n ∈ Finset.range (y / a), w n * F n a = ∑ n ∈ Finset.range y, w n * ∑ a ∈ Finset.Icc 1 (liuPanAbelSourceCutoff y X (n + 1)), F n a

Swapping a source sum with quotient prefixes replaces each prefix by one source aggregate at the cutoff A_{n+1}.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateAPPsiDiscrepancy_endpoint_shell (y X q l : ℕ) (f g : ℕ → ℝ) (hg0 : g 0 = 0) : (∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * g (y / a) * liuPanAPPsiDiscrepancy (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) else 0) = ∑ k ∈ Finset.Icc 1 y, g k * (liuPanAggregateAPPsiDiscrepancy k (liuPanAbelSourceCutoff y X k) q l f - liuPanAggregateAPPsiDiscrepancy k (liuPanAbelSourceCutoff y X (k + 1)) q l f)

Exact endpoint shell identity for the source-aggregated AP psi discrepancy.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateAPPsiDiscrepancy_inverseLog_endpoint_shell (y X q l : ℕ) (f : ℕ → ℝ) : (∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * (Real.log ↑(y / a))⁻¹ * liuPanAPPsiDiscrepancy (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) else 0) = ∑ k ∈ Finset.Icc 1 y, (Real.log ↑k)⁻¹ * (liuPanAggregateAPPsiDiscrepancy k (liuPanAbelSourceCutoff y X k) q l f - liuPanAggregateAPPsiDiscrepancy k (liuPanAbelSourceCutoff y X (k + 1)) q l f)

The endpoint shell identity at the inverse-log weight.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateAPPsiDiscrepancy_prefix_swap (y X q l : ℕ) (f w : ℕ → ℝ) : (∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * ∑ n ∈ Finset.range (y / a), w n * liuPanAPPsiDiscrepancy n q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) else 0) = ∑ n ∈ Finset.range y, w n * liuPanAggregateAPPsiDiscrepancy n (liuPanAbelSourceCutoff y X (n + 1)) q l f

Exact prefix swap for the source-aggregated AP psi discrepancy.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateAPPsiDiscrepancy_abel_prefix_swap (y X q l : ℕ) (f : ℕ → ℝ) : (∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * ∑ n ∈ Finset.range (y / a), liuPanInverseLogAbelWeight n * liuPanAPPsiDiscrepancy n q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) else 0) = ∑ n ∈ Finset.range y, liuPanInverseLogAbelWeight n * liuPanAggregateAPPsiDiscrepancy n (liuPanAbelSourceCutoff y X (n + 1)) q l f

The exact prefix swap at the nonnegative Abel weights used above.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPsiTerm (y X q l : ℕ) (f : ℕ → ℝ) : ℝ

The aggregate psi contribution after both exact finite rearrangements.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPsiTerm y X q l f = ∑ k ∈ Finset.Icc 1 y, (Real.log ↑k)⁻¹ * (MathlibNt.SieveTheory.LiuWeight.liuPanAggregateAPPsiDiscrepancy k (MathlibNt.SieveTheory.LiuWeight.liuPanAbelSourceCutoff y X k) q l f - MathlibNt.SieveTheory.LiuWeight.liuPanAggregateAPPsiDiscrepancy k (MathlibNt.SieveTheory.LiuWeight.liuPanAbelSourceCutoff y X (k + 1)) q l f) + ∑ n ∈ Finset.range y, MathlibNt.SieveTheory.LiuWeight.liuPanInverseLogAbelWeight n * MathlibNt.SieveTheory.LiuWeight.liuPanAggregateAPPsiDiscrepancy n (MathlibNt.SieveTheory.LiuWeight.liuPanAbelSourceCutoff y X (n + 1)) q l f

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogDeterministicTerm (kappa : ℝ) (y X q : ℕ) (f : ℕ → ℝ) : ℝ

The deterministic source-weighted difference between the discrete Abel main term and Liu's logarithmic integral.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogDeterministicTerm kappa y X q f = ∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * (MathlibNt.SieveTheory.LiuWeight.liuPanDiscreteInverseLogMain (y / a) - MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral kappa (↑y / ↑a)) else 0

theorem MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogDiscrepancy_eq_aggregateAbel (kappa : ℝ) (y X q l : ℕ) (f : ℕ → ℝ) (u v : ℕ) : liuPanCombinedInverseLogDiscrepancy (liuLogarithmicIntegral kappa) y X q l f u v = |liuPanAggregateInverseLogPsiTerm y X q l f + liuPanAggregateInverseLogDeterministicTerm kappa y X q f / ↑q.totient|

Exact aggregate-before-absolute-value decomposition of the combined inverse-log discrepancy. It remains valid for moduli 0 and 1.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogDiscrepancy_le_aggregateAbel (kappa : ℝ) (y X q l : ℕ) (f : ℕ → ℝ) (u v : ℕ) : liuPanCombinedInverseLogDiscrepancy (liuLogarithmicIntegral kappa) y X q l f u v ≤ |liuPanAggregateInverseLogPsiTerm y X q l f| + |liuPanAggregateInverseLogDeterministicTerm kappa y X q f| / ↑q.totient

The pointwise aggregate bound keeps the only analytic absolute value outside the full source convolution and separates the deterministic error.

Canonical aggregate maxima

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

Canonical reduced-residue maximum of the absolute aggregate psi term.

Equations

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

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPsiMaxY (X q x : ℕ) (f : ℕ → ℝ) : ℝ

Canonical maximum over y ≤ x of the absolute aggregate psi term.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPsiMaxY X q x f = (Finset.image (fun (y : ℕ) => MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPsiMaxL y X q f) (Finset.range (x + 1))).max' ⋯

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogDeterministicMaxL (kappa : ℝ) (y X q : ℕ) (f : ℕ → ℝ) : ℝ

Canonical reduced-residue maximum of the deterministic term. The term is independent of the residue, but the empty residue set at modulus zero is kept canonical.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogDeterministicMaxL kappa y X q f = if (AnalyticNumberTheory.Sieve.unitResidues q).Nonempty then |MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogDeterministicTerm kappa y X q f| else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogDeterministicMaxY (kappa : ℝ) (X q x : ℕ) (f : ℕ → ℝ) : ℝ

Canonical maximum over y ≤ x of the deterministic source error.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogDeterministicMaxY kappa X q x f = (Finset.image (fun (y : ℕ) => MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogDeterministicMaxL kappa y X q f) (Finset.range (x + 1))).max' ⋯

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPsiMaxL_zero (y X : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogPsiMaxL y X 0 f = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPsiMaxL_one (y X : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogPsiMaxL y X 1 f = |liuPanAggregateInverseLogPsiTerm y X 1 0 f|

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPsiMaxY_zero (X x : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogPsiMaxY X 0 x f = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPsiMaxY_one (X x : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogPsiMaxY X 1 x f = (Finset.image (fun (y : ℕ) => |liuPanAggregateInverseLogPsiTerm y X 1 0 f|) (Finset.range (x + 1))).max' ⋯

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogDeterministicMaxL_zero (kappa : ℝ) (y X : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogDeterministicMaxL kappa y X 0 f = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogDeterministicMaxL_one (kappa : ℝ) (y X : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogDeterministicMaxL kappa y X 1 f = |liuPanAggregateInverseLogDeterministicTerm kappa y X 1 f|

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogDeterministicMaxY_zero (kappa : ℝ) (X x : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogDeterministicMaxY kappa X 0 x f = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogDeterministicMaxY_one (kappa : ℝ) (X x : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogDeterministicMaxY kappa X 1 x f = (Finset.image (fun (y : ℕ) => |liuPanAggregateInverseLogDeterministicTerm kappa y X 1 f|) (Finset.range (x + 1))).max' ⋯

theorem MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogMaxL_le_aggregateAbel (kappa : ℝ) (y X q : ℕ) (f : ℕ → ℝ) (u v : ℕ) : liuPanCombinedInverseLogMaxL (liuLogarithmicIntegral kappa) y X q f u v ≤ liuPanAggregateInverseLogPsiMaxL y X q f + liuPanAggregateInverseLogDeterministicMaxL kappa y X q f / ↑q.totient

The pointwise aggregate bound lifted through the canonical residue maximum.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogMaxY_le_aggregateAbel (kappa : ℝ) (X q x : ℕ) (f : ℕ → ℝ) (u v : ℕ) : liuPanCombinedInverseLogMaxY (liuLogarithmicIntegral kappa) X q x f u v ≤ liuPanAggregateInverseLogPsiMaxY X q x f + liuPanAggregateInverseLogDeterministicMaxY kappa X q x f / ↑q.totient

The aggregate bound lifted through the canonical y maximum, without introducing any sourcewise triangle inequality.

Aggregate fixed-source and source-family bounds

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

The modulus-weighted aggregate psi average at a fixed source.

Equations

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

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

The separately visible modulus-weighted deterministic average.

Equations

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

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPsiBoundAt (N : ℕ) (f : ℕ → ℝ) (A B C : ℝ) : Prop

Fixed-N aggregate psi estimate, with the absolute value only after the source aggregation.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPsiBoundAt N f A B C = (MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateInverseLogPsiAverage N f B ≤ C * ↑N / Real.log ↑N ^ A)

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogDeterministicBoundAt (kappa : ℝ) (N : ℕ) (f : ℕ → ℝ) (A B C : ℝ) : Prop

Fixed-N deterministic source-error estimate.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogDeterministicBoundAt kappa N f A B C = (MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateInverseLogDeterministicAverage kappa N f B ≤ C * ↑N / Real.log ↑N ^ A)

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogSourceFamilyBound (kappa : ℝ) : Prop

The corrected aggregate source-family input. Its psi and deterministic components have separate constants and separate displayed bounds, while the source f_N is specialized inside the universal quantifier over N.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogSourceFamilyBound kappa = ∀ (A : ℝ), 0 < A → ∃ (Cpsi : ℝ), 0 < Cpsi ∧ ∃ (Cdet : ℝ), 0 < Cdet ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N0 : ℕ), ∀ (N : ℕ), N0 ≤ N → MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPsiBoundAt N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) A B Cpsi ∧ MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogDeterministicBoundAt kappa N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) A B Cdet

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanCombinedInverseLogAverage_le_aggregateAbel (kappa : ℝ) (N : ℕ) (B : ℝ) (u v : ℕ) : liuMainPanCombinedInverseLogAverage kappa N B u v ≤ liuMainPanAggregateInverseLogPsiAverage N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) B + liuMainPanAggregateInverseLogDeterministicAverage kappa N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) B

The exact combined average is bounded by the aggregate psi average plus the separate deterministic average.

theorem MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogSourceFamilyBound.to_combinedInverseLog {kappa : ℝ} (hagg : LiuMainPanAggregateInverseLogSourceFamilyBound kappa) (u v : ℕ) : LiuMainPanCombinedInverseLogSourceFamilyBound kappa u v

The corrected aggregate psi hypothesis together with its separately bounded deterministic component implies the combined inverse-log family bound. This theorem does not assert either analytic input.

Sourcewise diagnostic (analytically overstrong)

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPsiAbelMajorant (kappa : ℝ) (y : ℕ) (x : ℝ) (q l : ℕ) : ℝ

The pointwise Abel majorant. Its three summands are respectively the endpoint psi discrepancy divided by log y, a finite nonnegative weighted sum of prefix psi discrepancies, and the deterministic discrete-main error. Taking this majorant source by source is retained only for comparison; it is not the analytic frontier.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPsiAbelMajorant kappa y x q l = |MathlibNt.SieveTheory.LiuWeight.liuPanAPPsiDiscrepancy y q l| / Real.log ↑y + ∑ n ∈ Finset.range y, MathlibNt.SieveTheory.LiuWeight.liuPanInverseLogAbelWeight n * |MathlibNt.SieveTheory.LiuWeight.liuPanAPPsiDiscrepancy n q l| + |MathlibNt.SieveTheory.LiuWeight.liuPanDiscreteInverseLogMain y - MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral kappa x| / ↑q.totient

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPsiAbelMajorant_nonneg (kappa : ℝ) (y : ℕ) (x : ℝ) (q l : ℕ) : 0 ≤ liuPanPsiAbelMajorant kappa y x q l

theorem MathlibNt.SieveTheory.LiuWeight.abs_apLogVonMangoldt_sub_liuLogarithmicIntegral_le_psiAbelMajorant (kappa : ℝ) (y : ℕ) (x : ℝ) (q l : ℕ) : |AnalyticNumberTheory.Sieve.apLogVonMangoldt y q l - liuLogarithmicIntegral kappa x / ↑q.totient| ≤ liuPanPsiAbelMajorant kappa y x q l

Pointwise inverse-log discrepancy bound obtained from the exact Abel identity, with no distribution estimate assumed.

Diagnostic source-weighted maxima

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanSourceWeightedPsiAbelMajorant (kappa : ℝ) (y X q l : ℕ) (f : ℕ → ℝ) : ℝ

Diagnostic sourcewise Abel majorant. Although the source coefficient remains visible, the triangle inequality has already destroyed cancellation between distinct source indices.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanSourceWeightedPsiAbelMajorant kappa y X q l f = ∑ a ∈ Finset.Icc 1 X, if a.Coprime q then |f a| * MathlibNt.SieveTheory.LiuWeight.liuPanPsiAbelMajorant kappa (y / a) (↑y / ↑a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) else 0

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSourceWeightedPsiAbelMajorant_nonneg (kappa : ℝ) (y X q l : ℕ) (f : ℕ → ℝ) : 0 ≤ liuPanSourceWeightedPsiAbelMajorant kappa y X q l f

theorem MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogDiscrepancy_le_sourceWeightedPsiAbelMajorant (kappa : ℝ) (y X q l : ℕ) (f : ℕ → ℝ) (u v : ℕ) : liuPanCombinedInverseLogDiscrepancy (liuLogarithmicIntegral kappa) y X q l f u v ≤ liuPanSourceWeightedPsiAbelMajorant kappa y X q l f

The exact combined discrepancy is bounded by the diagnostic sourcewise majorant. This valid inequality is analytically too costly in the empty-progression tail.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanSourceWeightedPsiAbelMaxL (kappa : ℝ) (y X q : ℕ) (f : ℕ → ℝ) : ℝ

Canonical maximum of the source-weighted psi majorant over reduced residues.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanSourceWeightedPsiAbelMaxL kappa y X q f = if h : (AnalyticNumberTheory.Sieve.unitResidues q).Nonempty then (Finset.image (fun (l : ℕ) => MathlibNt.SieveTheory.LiuWeight.liuPanSourceWeightedPsiAbelMajorant kappa y X q l f) (AnalyticNumberTheory.Sieve.unitResidues q)).max' ⋯ else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanSourceWeightedPsiAbelMaxY (kappa : ℝ) (X q x : ℕ) (f : ℕ → ℝ) : ℝ

Canonical maximum of the source-weighted psi majorant over y ≤ x.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanSourceWeightedPsiAbelMaxY kappa X q x f = (Finset.image (fun (y : ℕ) => MathlibNt.SieveTheory.LiuWeight.liuPanSourceWeightedPsiAbelMaxL kappa y X q f) (Finset.range (x + 1))).max' ⋯

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSourceWeightedPsiAbelMaxL_zero (kappa : ℝ) (y X : ℕ) (f : ℕ → ℝ) : liuPanSourceWeightedPsiAbelMaxL kappa y X 0 f = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSourceWeightedPsiAbelMaxL_one (kappa : ℝ) (y X : ℕ) (f : ℕ → ℝ) : liuPanSourceWeightedPsiAbelMaxL kappa y X 1 f = liuPanSourceWeightedPsiAbelMajorant kappa y X 1 0 f

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSourceWeightedPsiAbelMaxY_zero (kappa : ℝ) (X x : ℕ) (f : ℕ → ℝ) : liuPanSourceWeightedPsiAbelMaxY kappa X 0 x f = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSourceWeightedPsiAbelMaxY_one (kappa : ℝ) (X x : ℕ) (f : ℕ → ℝ) : liuPanSourceWeightedPsiAbelMaxY kappa X 1 x f = (Finset.image (fun (y : ℕ) => liuPanSourceWeightedPsiAbelMajorant kappa y X 1 0 f) (Finset.range (x + 1))).max' ⋯

theorem MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogMaxL_le_sourceWeightedPsiAbelMaxL (kappa : ℝ) (y X q : ℕ) (f : ℕ → ℝ) (u v : ℕ) : liuPanCombinedInverseLogMaxL (liuLogarithmicIntegral kappa) y X q f u v ≤ liuPanSourceWeightedPsiAbelMaxL kappa y X q f

theorem MathlibNt.SieveTheory.LiuWeight.liuPanCombinedInverseLogMaxY_le_sourceWeightedPsiAbelMaxY (kappa : ℝ) (X q x : ℕ) (f : ℕ → ℝ) (u v : ℕ) : liuPanCombinedInverseLogMaxY (liuLogarithmicIntegral kappa) X q x f u v ≤ liuPanSourceWeightedPsiAbelMaxY kappa X q x f

Overstrong diagnostic source-family predicate

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

The source-weighted maximal psi functional averaged over Pan moduli.

Equations

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

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanPsiAbelBoundAt (kappa : ℝ) (N : ℕ) (f : ℕ → ℝ) (A B C : ℝ) : Prop

A fixed-N, fixed-source estimate for the overstrong sourcewise functional.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanPsiAbelBoundAt kappa N f A B C = (MathlibNt.SieveTheory.LiuWeight.liuMainPanPsiAbelAverage kappa N f B ≤ C * ↑N / Real.log ↑N ^ A)

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanPsiAbelSourceFamilyBound (kappa : ℝ) : Prop

An intentionally retained overstrong diagnostic, not the remaining analytic input. For q > y / a, the empty-progression contribution survives the sourcewise absolute value; averaged over reduced residues this prevents the claimed arbitrary logarithmic saving. The source weight f_N is nevertheless quantified correctly inside ∀ N, so finite consequences remain reusable.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanPsiAbelSourceFamilyBound kappa = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N0 : ℕ), ∀ (N : ℕ), N0 ≤ N → MathlibNt.SieveTheory.LiuWeight.LiuMainPanPsiAbelBoundAt kappa N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) A B C

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanCombinedInverseLogAverage_le_psiAbelAverage (kappa : ℝ) (N : ℕ) (B : ℝ) (u v : ℕ) : liuMainPanCombinedInverseLogAverage kappa N B u v ≤ liuMainPanPsiAbelAverage kappa N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) B

The overstrong diagnostic functional dominates the combined inverse-log average for every fixed N.

theorem MathlibNt.SieveTheory.LiuWeight.LiuMainPanPsiAbelSourceFamilyBound.to_combinedInverseLog {kappa : ℝ} (hpsi : LiuMainPanPsiAbelSourceFamilyBound kappa) (u v : ℕ) : LiuMainPanCombinedInverseLogSourceFamilyBound kappa u v

The overstrong diagnostic predicate has the stated finite implication. It is not proposed as the analytic Bombieri--Vinogradov frontier.