Main-parametric Pan consumption for Liu's coprime majorant

This module defines the fixed-parameter Pan objects for an arbitrary main-term model and proves the finite structural implication needed by Liu's coprime eqn-r lane. It does not assert the analytic Pan mean-value theorem.

The residue maximum uses the live ANT unitResidues convention. In particular, the unique canonical residue modulo 1 is 0.

Main-parametric finite Pan objects

theorem MathlibNt.SieveTheory.LiuWeight.liuScaledAPError_sub_normalization (κ₂ κ₁ : ℝ) (Y a q l : ℕ) : liuScaledAPError (liuLogarithmicIntegral κ₂) Y a q l - liuScaledAPError (liuLogarithmicIntegral κ₁) Y a q l = -(κ₂ - κ₁) / ↑q.totient

Exact change in a scaled AP error when only the additive normalization of the logarithmic integral is changed.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuMainPanInnerSum (main : ℝ → ℝ) (Y X q l : ℕ) (f : ℕ → ℝ) : ℝ

The unrestricted Pan inner sum for an arbitrary main-term model.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainPanInnerSum main Y X q l f = ∑ a ∈ Finset.range (X + 1), f a * MathlibNt.SieveTheory.LiuWeight.liuScaledAPError main Y a q l

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeSum (main : ℝ → ℝ) (Y X q l : ℕ) (f : ℕ → ℝ) : ℝ

The coprime Pan inner sum for an arbitrary main-term model.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeSum main Y X q l f = ∑ a ∈ Finset.range (X + 1), if a.Coprime q then f a * MathlibNt.SieveTheory.LiuWeight.liuScaledAPError main Y a q l else 0

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

The source-interval version of the coprime Pan sum, with Pan's convention A₁ < a ≤ A₂.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeIntervalSum main Y A₁ A₂ q l f = ∑ a ∈ Finset.Ioc A₁ A₂, if a.Coprime q then f a * MathlibNt.SieveTheory.LiuWeight.liuScaledAPError main Y a q l else 0

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeSum_eq_sourceIntervalSum (main : ℝ → ℝ) (Y X A₁ A₂ q l : ℕ) (f : ℕ → ℝ) (hA₂X : A₂ ≤ X) (hsupp : ∀ a ≤ X, f a ≠ 0 → A₁ < a ∧ a ≤ A₂) : liuMainPanCoprimeSum main Y X q l f = liuMainPanCoprimeIntervalSum main Y A₁ A₂ q l f

Zero extension from a Pan source interval to the ambient finite range does not alter the coprime aggregate. This is the finite support bridge required before applying Corollary (2.30).

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuMainPanMaxL (main : ℝ → ℝ) (Y X q : ℕ) (f : ℕ → ℝ) : ℝ

The maximum of the absolute coprime inner sum over canonical reduced residues modulo q. The value at q = 0 is 0, while q = 1 uses residue 0.

Equations

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

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuMainPanMaxY (main : ℝ → ℝ) (X q N : ℕ) (f : ℕ → ℝ) : ℝ

The maximum of liuMainPanMaxL over source parameters Y ≤ N.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainPanMaxY main X q N f = (Finset.image (fun (Y : ℕ) => MathlibNt.SieveTheory.LiuWeight.liuMainPanMaxL main Y X q f) (Finset.range (N + 1))).max' ⋯

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

The Pan modulus cutoff ⌊N^(1/2) / log(N)^B⌋.

Equations

• MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B = ⌊↑N ^ (1 / 2) / Real.log ↑N ^ B⌋₊

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuSourceDEpsilon_le_panModulusCutoff (ε B : ℝ) (hε : 0 < ε) (_hB : 0 ≤ B) : ∀ᶠ (N : ℕ) in Filter.atTop, liuSourceDEpsilon N ε ≤ panModulusCutoff N B

Liu's source cutoff is eventually contained in Pan's modulus range.

theorem MathlibNt.SieveTheory.LiuWeight.exists_liuSourceDEpsilon_le_panModulusCutoff (ε B : ℝ) (hε : 0 < ε) (hB : 0 ≤ B) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → liuSourceDEpsilon N ε ≤ panModulusCutoff N B

Existential threshold form of the eventual Liu-to-Pan cutoff inclusion.

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

The fixed-N main-parametric Pan weighted sum.

Equations

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

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

The endpoint-only weighted sum at Y = N. This is the exact prefix needed by Liu's source-Q consumer and avoids strengthening Pan--Ding--Wang's source interval hypotheses to every small prefix.

Equations

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

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

Fixed-N endpoint form of the weighted Pan mean-value inequality.

Equations

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

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

A transparent fixed-N instance of the main-parametric Pan mean-value inequality. This is a predicate for consuming an analytic input, not a proof of that input.

Equations

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

Proxy compatibility

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanInnerSum_proxy (Y X q l : ℕ) (f : ℕ → ℝ) : liuMainPanInnerSum AnalyticNumberTheory.Sieve.logarithmicIntegral Y X q l f = AnalyticNumberTheory.Sieve.panDistributionFullSum Y X q l f

Proxy compatibility. The unrestricted object specializes to ANT's historical x / log x finite sum. This is not a true-li statement.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeSum_proxy (Y X q l : ℕ) (f : ℕ → ℝ) : liuMainPanCoprimeSum AnalyticNumberTheory.Sieve.logarithmicIntegral Y X q l f = AnalyticNumberTheory.Sieve.panDistributionSum Y X q l f

Proxy compatibility. The coprime object specializes to ANT's historical x / log x finite sum. This is not a true-li statement.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeSum_eq_liuMainCoprimeSum (main : ℝ → ℝ) (Y X q l : ℕ) (f : ℕ → ℝ) : liuMainPanCoprimeSum main Y X q l f = liuMainCoprimeSum main Y X q l f

The new coprime sum is definitionally the coprime sum used by the Liu source-Q majorant.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanMaxL_proxy (Y X q : ℕ) (f : ℕ → ℝ) : liuMainPanMaxL AnalyticNumberTheory.Sieve.logarithmicIntegral Y X q f = AnalyticNumberTheory.Sieve.panMaxL Y X q f

Proxy compatibility. The canonical-residue maximum specializes definitionally to ANT's live panMaxL.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanMaxY_proxy (X q N : ℕ) (f : ℕ → ℝ) : liuMainPanMaxY AnalyticNumberTheory.Sieve.logarithmicIntegral X q N f = AnalyticNumberTheory.Sieve.panMaxY X q N f

Proxy compatibility. The source-parameter maximum specializes definitionally to ANT's live panMaxY.

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanMaxL_one (main : ℝ → ℝ) (Y X : ℕ) (f : ℕ → ℝ) : liuMainPanMaxL main Y X 1 f = |liuMainPanCoprimeSum main Y X 1 0 f|

In particular, the modulus-one maximum uses the canonical residue 0.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanWeightedSum_proxy (N : ℕ) (f : ℕ → ℝ) (B : ℝ) : liuMainPanWeightedSum AnalyticNumberTheory.Sieve.logarithmicIntegral N f B = ∑ q ∈ Finset.range (panModulusCutoff N B + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * AnalyticNumberTheory.Sieve.panMaxY N q N f

Proxy compatibility. The fixed weighted sum specializes to the finite left side occurring in ANT's PanMeanValueUniform.

theorem MathlibNt.SieveTheory.LiuWeight.LiuMainPanMeanValueAt_proxy (N : ℕ) (f : ℕ → ℝ) (A B C : ℝ) : LiuMainPanMeanValueAt AnalyticNumberTheory.Sieve.logarithmicIntegral N f A B C ↔ ∑ q ∈ Finset.range (panModulusCutoff N B + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * AnalyticNumberTheory.Sieve.panMaxY N q N f ≤ C * ↑N / Real.log ↑N ^ A

Proxy compatibility. This is only a fixed-N restatement of ANT's historical proxy finite inequality, not an analytic theorem.

Finite consumption bridge

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanMaxL_nonneg (main : ℝ → ℝ) (Y X q : ℕ) (f : ℕ → ℝ) : 0 ≤ liuMainPanMaxL main Y X q f

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanMaxY_nonneg (main : ℝ → ℝ) (X q N : ℕ) (f : ℕ → ℝ) : 0 ≤ liuMainPanMaxY main X q N f

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuMainPanCoprimeSum_le_maxL (main : ℝ → ℝ) (Y X q l : ℕ) (f : ℕ → ℝ) (hl : l ∈ AnalyticNumberTheory.Sieve.unitResidues q) : |liuMainPanCoprimeSum main Y X q l f| ≤ liuMainPanMaxL main Y X q f

A canonical reduced residue is bounded by the residue maximum at the same endpoint.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuMainPanCoprimeSum_le_maxY (main : ℝ → ℝ) (Y X q N l : ℕ) (f : ℕ → ℝ) (hY : Y ≤ N) (hl : l ∈ AnalyticNumberTheory.Sieve.unitResidues q) : |liuMainPanCoprimeSum main Y X q l f| ≤ liuMainPanMaxY main X q N f

A canonical reduced residue and a source parameter in range are bounded by the two nested Pan maxima.

theorem MathlibNt.SieveTheory.LiuWeight.liuPaperQCoprimeRBound_of_liuMainPanEndpointMeanValueAt (main : ℝ → ℝ) (N : ℕ) (ε A B C : ℝ) (hcut : liuSourceDEpsilon N ε ≤ panModulusCutoff N B) (hpan : LiuMainPanEndpointMeanValueAt main N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B C) : LiuPaperQCoprimeRBound main N ε A C

The source-faithful endpoint structural bridge: Pan's weighted estimate at Y = N already controls the only prefix used by Liu's source-Q coprime majorant. No maximum over unsupported small prefixes is needed.

theorem MathlibNt.SieveTheory.LiuWeight.liuPaperQCoprimeRBound_of_liuMainPanMeanValueAt (main : ℝ → ℝ) (N : ℕ) (ε A B C : ℝ) (hcut : liuSourceDEpsilon N ε ≤ panModulusCutoff N B) (hpan : LiuMainPanMeanValueAt main N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B C) : LiuPaperQCoprimeRBound main N ε A C

The exact structural consumption bridge: a fixed-N, main-parametric Pan mean-value inequality controls Liu's source-Q coprime majorant whenever its source divisor cutoff is inside the Pan modulus cutoff.

theorem MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral_liuPaperQCoprimeRBound_of_panMeanValueAt (κ : ℝ) (N : ℕ) (ε A B C : ℝ) (hcut : liuSourceDEpsilon N ε ≤ panModulusCutoff N B) (hpan : LiuMainPanMeanValueAt (liuLogarithmicIntegral κ) N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B C) : LiuPaperQCoprimeRBound (liuLogarithmicIntegral κ) N ε A C

The genuine logarithmic-integral specialization retains both the analytic fixed-N Pan predicate and the cutoff inclusion as explicit hypotheses.

theorem MathlibNt.SieveTheory.LiuWeight.exists_liuLogarithmicIntegral_liuPaperQCoprimeRBound_of_panMeanValueAt (ε B : ℝ) (hε : 0 < ε) (hB : 0 ≤ B) : ∃ (N₀ : ℕ), ∀ (N : ℕ) (κ A C : ℝ), N₀ ≤ N → LiuMainPanMeanValueAt (liuLogarithmicIntegral κ) N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B C → LiuPaperQCoprimeRBound (liuLogarithmicIntegral κ) N ε A C

Beyond a threshold depending only on ε and B, the true logarithmic- integral coprime bound requires only the fixed-N Pan mean-value input.

theorem MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceCoprimeDistributionMajorant_li_normalization_le (κ₂ κ₁ : ℝ) (N : ℕ) (ε : ℝ) : liuPaperQSourceCoprimeDistributionMajorant (liuLogarithmicIntegral κ₂) N ε ≤ liuPaperQSourceCoprimeDistributionMajorant (liuLogarithmicIntegral κ₁) N ε + (|κ₂ - κ₁| * ∑ a ∈ Finset.Icc 1 N, liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a) * paperQStyleFullDivisorWeightSum N (paperQSourceCutoff N ε)

Changing only the additive normalization of the genuine logarithmic integral costs the source mass times the full paper-Q divisor weight.

theorem MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceCoprimeDistributionMajorant_li_normalization_le_rpow (κ₂ κ₁ : ℝ) (N : ℕ) (ε : ℝ) (hN : 3 ≤ N) (hε : 0 ≤ ε) : liuPaperQSourceCoprimeDistributionMajorant (liuLogarithmicIntegral κ₂) N ε ≤ liuPaperQSourceCoprimeDistributionMajorant (liuLogarithmicIntegral κ₁) N ε + 3 * paperQStyleDivisorWeightLogConstant * |κ₂ - κ₁| * ↑N ^ (2 / 3) * Real.log ↑N ^ 3

Explicit finite N^(2/3) log^3 N normalization-loss bound.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_mul_rpow_two_thirds_log_cube_le_div_log_rpow (C A : ℝ) (hC : 0 ≤ C) : ∀ᶠ (N : ℕ) in Filter.atTop, C * ↑N ^ (2 / 3) * Real.log ↑N ^ 3 ≤ ↑N / Real.log ↑N ^ A

Any fixed multiple of N^(2/3) log^3 N is eventually absorbed by N / log^A N, for an arbitrary fixed real logarithmic exponent A.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuPaperQSourceCoprimeDistributionMajorant_li_normalization_le (κ₂ κ₁ ε A : ℝ) (hε : 0 ≤ ε) : ∀ᶠ (N : ℕ) in Filter.atTop, liuPaperQSourceCoprimeDistributionMajorant (liuLogarithmicIntegral κ₂) N ε ≤ liuPaperQSourceCoprimeDistributionMajorant (liuLogarithmicIntegral κ₁) N ε + ↑N / Real.log ↑N ^ A

The additive-normalization loss in the aggregate coprime Pan majorant is eventually absorbable into any prescribed inverse logarithmic power.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuPaperQSourceCoprimeDistributionMajorant_li_normalization_transfer (κ₂ κ₁ ε A C : ℝ) (hε : 0 ≤ ε) (hκ₁ : ∀ᶠ (N : ℕ) in Filter.atTop, liuPaperQSourceCoprimeDistributionMajorant (liuLogarithmicIntegral κ₁) N ε ≤ C * ↑N / Real.log ↑N ^ A) : ∀ᶠ (N : ℕ) in Filter.atTop, liuPaperQSourceCoprimeDistributionMajorant (liuLogarithmicIntegral κ₂) N ε ≤ (C + 1) * ↑N / Real.log ↑N ^ A

Consequently, an eventual inverse-log bound for one additive normalization transfers to every other normalization, at the cost of adding 1 to the fixed constant.