Canonical Pan--Wang--Ding source theorem interface

This module records the weighted aggregate residue-class interface motivated by Corollary (2.30) of Pan--Ding--Wang (1975), deduced there from Theorem 2 (1.2). The corollary carries the squarefree modulus weight 3^ν(q) |μ(q)| and is uniform over coefficient functions with |f(a)| ≤ 1; hence varying Chen sources are compatible with its quantifier order. The source gives the concrete choice B = 2A + 24; the interface below existentially weakens that value.

The endpoint interface below uses only y = x = N, which is the sole prefix consumed by Liu's eqn-r lane. This avoids the previous, unsupported strengthening to every small natural prefix. Two source-correspondence bridges remain separate: the zero-extended liuWeight must be identified with a source interval log^(2B) N < A₁ ≤ a ≤ A₂ < N^(1-ε), and the paper's unspecified additive normalization of li must be related to the chosen normalization.

The analytic theorem itself remains an explicit proposition. No primitive- character L¹ majorant is inferred from it: such a majorant is strictly stronger and suffers a genuine weighted-conductor resonance obstruction.

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

Natural cutoff whose range represents the source's strict real inequality.

Equations

• MathlibNt.SieveTheory.LiuWeight.panSourceStrictModulusCutoff N B = ⌈↑N ^ (1 / 2) / Real.log ↑N ^ B⌉₊

theorem MathlibNt.SieveTheory.LiuWeight.mem_range_panSourceStrictModulusCutoff_iff (q N : ℕ) (B : ℝ) : q ∈ Finset.range (panSourceStrictModulusCutoff N B) ↔ ↑q < ↑N ^ (1 / 2) / Real.log ↑N ^ B

Membership in the source cutoff is exactly the paper's strict real inequality; in particular this also handles the case where the real endpoint is an integer.

theorem MathlibNt.SieveTheory.LiuWeight.range_panModulusCutoff_add_one_subset_sourceStrict (N : ℕ) (B : ℝ) (hN : 0 < N) (hlog : 1 < Real.log ↑N) : Finset.range (panModulusCutoff N (B + 1) + 1) ⊆ Finset.range (panSourceStrictModulusCutoff N B)

Once log N > 1, every modulus in Lean's closed floor cutoff with exponent B+1 satisfies the source's strict real cutoff with exponent B.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_range_panModulusCutoff_add_one_subset_sourceStrict (B : ℝ) : ∀ᶠ (N : ℕ) in Filter.atTop, Finset.range (panModulusCutoff N (B + 1) + 1) ⊆ Finset.range (panSourceStrictModulusCutoff N B)

For each fixed paper exponent B, using B+1 in the existing Lean cutoff is eventually source-faithful at the strict endpoint.

theorem MathlibNt.SieveTheory.LiuWeight.exists_range_panModulusCutoff_add_one_subset_sourceStrict (B : ℝ) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Finset.range (panModulusCutoff N (B + 1) + 1) ⊆ Finset.range (panSourceStrictModulusCutoff N B)

Threshold form of the eventual strict-endpoint bridge.

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

Integer lower endpoint used to place Liu's zero-extended source inside the strict interval required by Pan--Ding--Wang.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanSourceIntervalLower N B = ⌊Real.log ↑N ^ (2 * B)⌋₊ + 1

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanSourceIntervalUpper (N : ℕ) : ℕ

Integer upper endpoint at Liu's exact two-thirds support scale.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanSourceIntervalUpper N = ⌊↑N ^ (2 / 3)⌋₊

theorem MathlibNt.SieveTheory.LiuWeight.log_rpow_lt_liuPanSourceIntervalLower (N : ℕ) (B : ℝ) : Real.log ↑N ^ (2 * B) < ↑(liuPanSourceIntervalLower N B)

The lower endpoint is strictly above the logarithmic source threshold.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSourceIntervalUpper_lt_rpow_three_fourths {N : ℕ} (hN : 1 < N) : ↑(liuPanSourceIntervalUpper N) < ↑N ^ (3 / 4)

For N > 1, the two-thirds upper endpoint is strictly below the fixed N^(3/4) source ceiling used in the Pan corollary.

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceZ10_le_liuPanSourceIntervalUpper {N : ℕ} (hN : 1 ≤ N) : liuSourceZ10 N ≤ liuPanSourceIntervalUpper N

Liu's tenth-power source cutoff lies below the two-thirds Pan endpoint.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuPanSourceIntervalLower_lt_liuSourceZ10 (B : ℝ) : ∀ᶠ (N : ℕ) in Filter.atTop, liuPanSourceIntervalLower N B < liuSourceZ10 N

For every fixed Pan exponent, the logarithmic lower endpoint is eventually strictly below Liu's N^(1/10) source cutoff.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuPanSourceInterval_hypotheses (B : ℝ) : ∀ᶠ (N : ℕ) in Filter.atTop, Real.log ↑N ^ (2 * B) < ↑(liuPanSourceIntervalLower N B) ∧ liuPanSourceIntervalLower N B ≤ liuPanSourceIntervalUpper N ∧ ↑(liuPanSourceIntervalUpper N) < ↑N ^ (3 / 4) ∧ ∀ (a : ℕ), |liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a| ≤ 1

All source-side interval and coefficient hypotheses needed for the Liu specialization of Corollary (2.30) hold eventually (with paper ε = 1/4).

theorem MathlibNt.SieveTheory.LiuWeight.liuWeight_support_mem_panSourceInterval {N a : ℕ} {B : ℝ} (hlow : liuPanSourceIntervalLower N B < liuSourceZ10 N) (ha : liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a ≠ 0) : a ∈ Finset.Ioc (liuPanSourceIntervalLower N B) (liuPanSourceIntervalUpper N)

Conditional finite support bridge. Once the logarithmic lower endpoint is below Liu's N^(1/10) cutoff, every nonzero source coefficient lies in the Pan interval (A₁,A₂].

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeSum_eq_panSourceInterval (main : ℝ → ℝ) {N q l : ℕ} {B : ℝ} (hN : 1 ≤ N) (hlow : liuPanSourceIntervalLower N B < liuSourceZ10 N) : liuMainPanCoprimeSum main N N q l (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) = liuMainPanCoprimeIntervalSum main N (liuPanSourceIntervalLower N B) (liuPanSourceIntervalUpper N) q l (liuWeight N (liuSourceZ10 N) (liuSourceY3 N))

At a fixed endpoint, Liu's zero-extended coprime source sum is exactly the Pan interval sum once the eventual logarithmic lower-cutoff inequality holds.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuMainPanCoprimeSum_eq_panSourceInterval (main : ℝ → ℝ) (B : ℝ) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (q l : ℕ), liuMainPanCoprimeSum main N N q l (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) = liuMainPanCoprimeIntervalSum main N (liuPanSourceIntervalLower N B) (liuPanSourceIntervalUpper N) q l (liuWeight N (liuSourceZ10 N) (liuSourceY3 N))

Eventual source-interval identity for every modulus and residue.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeIntervalMaxL (main : ℝ → ℝ) (Y A₁ A₂ q : ℕ) (f : ℕ → ℝ) : ℝ

The residue-class maximum in the literal source-interval formulation of Pan--Ding--Wang, Corollary (2.30).

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeIntervalMaxL main Y A₁ A₂ q f = if h : (AnalyticNumberTheory.Sieve.unitResidues q).Nonempty then (Finset.image (fun (l : ℕ) => |MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeIntervalSum main Y A₁ A₂ q l f|) (AnalyticNumberTheory.Sieve.unitResidues q)).max' ⋯ else 0

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

The literal left side of Corollary (2.30), instantiated with Liu's source interval and retaining the paper's strict real modulus cutoff.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanWangDingCorollary230Sum κ N B = ∑ q ∈ Finset.range (MathlibNt.SieveTheory.LiuWeight.panSourceStrictModulusCutoff N B), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeIntervalMaxL (MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral κ) N (MathlibNt.SieveTheory.LiuWeight.liuPanSourceIntervalLower N B) (MathlibNt.SieveTheory.LiuWeight.liuPanSourceIntervalUpper N) q (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N))

def MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingCorollary230 : Prop

Source-faithful Liu specialization of Pan--Ding--Wang, Corollary (2.30). This is the consequence consumed by the eqn-r lane, not a formalization of the paper's more general arbitrary-f, arbitrary-interval statement. The additive normalization of li is fixed but unspecified by the source, while the source exponent (the paper permits B = 2A + 24) is existentially weakened.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingCorollary230 = ∃ (κ_src : ℝ), ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → MathlibNt.SieveTheory.LiuWeight.liuPanWangDingCorollary230Sum κ_src N B ≤ C * ↑N / Real.log ↑N ^ A

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingCorollary230.to_coprimeRBound (hPan : LiuPanWangDingCorollary230) (ε A : ℝ) (hε : 0 < ε) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → LiuPaperQCoprimeRBound (liuLogarithmicIntegral 2) N ε A C

The literal source contract transports all the way to Liu's canonical κ = 2 coprime consumer. The source cutoff exponent B becomes B+1 at the closed-floor endpoint, and the fixed normalization discrepancy is absorbed in one further copy of N / log^A N.

def MathlibNt.SieveTheory.LiuWeight.LiuPanCanonicalCoprimeTheorem : Prop

The exact downstream analytic interface needed after source transport: every positive ε,A admits an eventual canonical-li₂ coprime eqn-r bound.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuPanCanonicalCoprimeTheorem = ∀ (ε A : ℝ), 0 < ε → 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → MathlibNt.SieveTheory.LiuWeight.LiuPaperQCoprimeRBound (MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral 2) N ε A C

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingCorollary230.to_canonicalCoprimeTheorem (hPan : LiuPanWangDingCorollary230) : LiuPanCanonicalCoprimeTheorem

The literal source corollary supplies the exact canonical consumer interface, without identifying its unspecified additive normalization with 2.

def MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingSourceMeanValue (κ : ℝ) : Prop

A post-transport endpoint contract at a specified additive normalization. It is convenient for downstream consumers, but is not the literal statement of Corollary (2.30): the source-faithful Liu specialization is LiuPanWangDingCorollary230, with a strict modulus cutoff, source interval, and existential source normalization.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingSourceMeanValue κ = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → MathlibNt.SieveTheory.LiuWeight.LiuMainPanEndpointMeanValueAt (MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral κ) N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) A B C

def MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingTheorem : Prop

A stronger conditional convenience contract at canonical normalization li₂(x) = 2 + ∫₂ˣ dt / log t. This is not identified definitionally with the source-literal Corollary (2.30); use LiuPanWangDingCorollary230.to_coprimeRBound for the source-faithful route.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingTheorem = MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingSourceMeanValue 2

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingSourceMeanValue.to_coprimeRBound {κ : ℝ} (hPan : LiuPanWangDingSourceMeanValue κ) (ε A : ℝ) (hε : 0 < ε) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → LiuPaperQCoprimeRBound (liuLogarithmicIntegral κ) N ε A C

The aggregate Pan--Wang--Ding source theorem directly supplies Liu's source-Q coprime remainder bound. The only additional step is the already proved eventual inclusion of Liu's divisor cutoff in Pan's modulus range.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingTheorem.to_coprimeRBound (hPan : LiuPanWangDingTheorem) (ε A : ℝ) (hε : 0 < ε) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → LiuPaperQCoprimeRBound (liuLogarithmicIntegral 2) N ε A C

Consumer consequence of the stronger conditional canonical contract.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingTheorem.to_canonicalCoprimeTheorem (hPan : LiuPanWangDingTheorem) : LiuPanCanonicalCoprimeTheorem

The stronger canonical endpoint contract also supplies the minimal canonical consumer interface.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanCanonicalCoprimeTheorem.eventually_liuPaperQSourceFullDistributionMajorant_le (hPan : LiuPanCanonicalCoprimeTheorem) (ε A : ℝ) (hε : 0 < ε) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → liuPaperQSourceFullDistributionMajorant (liuLogarithmicIntegral 2) N ε ≤ C * ↑N / Real.log ↑N ^ A

The canonical coprime consumer interface implies every fixed logarithmic saving for Liu's exact eqn-r source sum. The full majorant keeps 3^ω(d) outside the absolute value of each inner residue-class error.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingTheorem.eventually_liuPaperQSourceFullDistributionMajorant_le (hPan : LiuPanWangDingTheorem) (ε A : ℝ) (hε : 0 < ε) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → liuPaperQSourceFullDistributionMajorant (liuLogarithmicIntegral 2) N ε ≤ C * ↑N / Real.log ↑N ^ A

Backward-compatible wrapper for the stronger canonical endpoint contract.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingCorollary230.eventually_liuPaperQSourceFullDistributionMajorant_le (hPan : LiuPanWangDingCorollary230) (ε A : ℝ) (hε : 0 < ε) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → liuPaperQSourceFullDistributionMajorant (liuLogarithmicIntegral 2) N ε ≤ C * ↑N / Real.log ↑N ^ A

Source-faithful wrapper from literal Corollary (2.30) to the same full canonical consumer majorant.