Exact split of Liu's signed Pan residual

This module separates the existing signed residual into its two exact analytic inputs. The signed-main absolute value remains outside the complete source-faithful combination; it is not split termwise. The second input retains the AP prime-power correction, the exact source weight, both maxima, and the original modulus weight and cutoff.

For the full Pan family these inputs are required for every fixed A > 0. For the final M1 use, it is enough analytically to obtain a residual o(N / log(N)^2) or O(N / log(N)^(2 + delta)); no existing contract is changed here.

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

The maximum over coprime residues of the absolute value of the complete source-faithful signed-main sum. The absolute value is not distributed across the terms of liuPanSignedMainKernel.

Equations

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

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

The maximum of the complete signed-main residue maximum over y ≤ x.

Equations

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

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

The maximum over coprime residues of the exact AP prime-power correction with the source weight retained inside liuPanSignedCorrectionBound.

Equations

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

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

The maximum of the AP prime-power correction over y ≤ x.

Equations

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

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSignedMainMaxL_nonneg (distMain : ℝ → ℝ) (y X q : ℕ) (f : ℕ → ℝ) (u v : ℕ) : 0 ≤ liuPanSignedMainMaxL distMain y X q f u v

The complete signed-main residue maximum is nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSignedMainMaxY_nonneg (distMain : ℝ → ℝ) (X q x : ℕ) (f : ℕ → ℝ) (u v : ℕ) : 0 ≤ liuPanSignedMainMaxY distMain X q x f u v

The complete signed-main y-maximum is nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAPPrimePowerCorrectionMaxL_nonneg (y X q : ℕ) (f : ℕ → ℝ) : 0 ≤ liuPanAPPrimePowerCorrectionMaxL y X q f

The AP prime-power residue maximum is nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAPPrimePowerCorrectionMaxY_nonneg (X q x : ℕ) (f : ℕ → ℝ) : 0 ≤ liuPanAPPrimePowerCorrectionMaxY X q x f

The AP prime-power y-maximum is nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSignedResidualMaxY_le_split (distMain : ℝ → ℝ) (X q x : ℕ) (f : ℕ → ℝ) (u v : ℕ) : liuPanSignedResidualMaxY distMain X q x f u v ≤ liuPanSignedMainMaxY distMain X q x f u v + liuPanAPPrimePowerCorrectionMaxY X q x f

The audited residual maximum is bounded by the sum of its two exact component maxima. Only the two finite maxima are split; the signed-main absolute value remains intact.

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanSignedMainBoundAt (distMain : ℝ → ℝ) (N : ℕ) (f : ℕ → ℝ) (A B Cmain : ℝ) (u v : ℕ) : Prop

Fixed-N bound for the complete signed-main average. This retains one absolute value around the entire source-faithful signed sum.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanSignedMainBoundAt distMain N f A B Cmain u v = (∑ q ∈ Finset.range (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * MathlibNt.SieveTheory.LiuWeight.liuPanSignedMainMaxY distMain N q N f u v ≤ Cmain * ↑N / Real.log ↑N ^ A)

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

Fixed-N bound for the AP prime-power correction average, with the exact source weight, modulus cutoff, arithmetic weight, and both maxima retained.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanAPPrimePowerCorrectionBoundAt N f A B Cpp = (∑ 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 ≤ Cpp * ↑N / Real.log ↑N ^ A)

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanSignedMain_average_nonneg (distMain : ℝ → ℝ) (N : ℕ) (f : ℕ → ℝ) (B : ℝ) (u v : ℕ) : 0 ≤ ∑ q ∈ Finset.range (panModulusCutoff N B + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * liuPanSignedMainMaxY distMain N q N f u v

The complete signed-main weighted average is nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanAPPrimePowerCorrection_average_nonneg (N : ℕ) (f : ℕ → ℝ) (B : ℝ) : 0 ≤ ∑ q ∈ Finset.range (panModulusCutoff N B + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * liuPanAPPrimePowerCorrectionMaxY N q N f

The AP prime-power correction weighted average is nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.LiuMainPanSignedResidualBoundAt.of_splitBoundsAt {distMain : ℝ → ℝ} {N : ℕ} {f : ℕ → ℝ} {A B Cmain Cpp : ℝ} {u v : ℕ} (hmain : LiuMainPanSignedMainBoundAt distMain N f A B Cmain u v) (hpp : LiuMainPanAPPrimePowerCorrectionBoundAt N f A B Cpp) : LiuMainPanSignedResidualBoundAt distMain N f A B (Cmain + Cpp) u v

The two exact fixed-N component bounds imply the existing signed residual bound with the sum of constants and unchanged parameters and cutoff.

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanSignedResidualSplitSourceFamilyInputs (distMain : ℝ → ℝ) (A B Cmain Cpp : ℝ) (u v : ℕ) : Prop

Eventual source-family packaging of the two fixed-N components. The parameters A, B, Cmain, Cpp, u, and v are fixed before N → ∞.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanSignedResidualSplitSourceFamilyInputs distMain A B Cmain Cpp u v = ∀ᶠ (N : ℕ) in Filter.atTop, MathlibNt.SieveTheory.LiuWeight.LiuMainPanSignedMainBoundAt distMain N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) A B Cmain u v ∧ MathlibNt.SieveTheory.LiuWeight.LiuMainPanAPPrimePowerCorrectionBoundAt N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) A B Cpp

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuMainPanSignedResidualBoundAt_of_splitBoundsAt {distMain : ℝ → ℝ} {A B Cmain Cpp : ℝ} {u v : ℕ} (hmain : ∀ᶠ (N : ℕ) in Filter.atTop, LiuMainPanSignedMainBoundAt distMain N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B Cmain u v) (hpp : ∀ᶠ (N : ℕ) in Filter.atTop, LiuMainPanAPPrimePowerCorrectionBoundAt N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B Cpp) : ∀ᶠ (N : ℕ) in Filter.atTop, LiuMainPanSignedResidualBoundAt distMain N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B (Cmain + Cpp) u v

Eventual component bounds, each quantified after all analytic parameters, give the eventual existing residual bound.

theorem MathlibNt.SieveTheory.LiuWeight.LiuMainPanSignedResidualSplitSourceFamilyInputs.signedResidual {distMain : ℝ → ℝ} {A B Cmain Cpp : ℝ} {u v : ℕ} (h : LiuMainPanSignedResidualSplitSourceFamilyInputs distMain A B Cmain Cpp u v) : ∀ᶠ (N : ℕ) in Filter.atTop, LiuMainPanSignedResidualBoundAt distMain N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) A B (Cmain + Cpp) u v

The packaged split source-family input implies the existing eventual residual input with constants added.