Source-faithful signed Pan assembly for arbitrary distribution mains

This is the finite Vaughan/Chebyshev decomposition used by the Liu eqn-r lane, with the distribution main left as an explicit parameter. In particular, the genuine logarithmic integral is never identified with ANT's historical x / log x compatibility function.

Exact signed kernels

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanSignedMainKernel (distMain : ℝ → ℝ) (y a q l u v : ℕ) : ℝ

The exact source-faithful signed residual after the aggregate Type I and Type II kernels have been removed.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanSignedMainKernel distMain y a q l u v = AnalyticNumberTheory.Sieve.apV1Log (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) u - AnalyticNumberTheory.Sieve.apV1 (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) u / Real.log ↑(y / a) + (AnalyticNumberTheory.Sieve.apV3Log (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) u v - AnalyticNumberTheory.Sieve.apV3 (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) u v / Real.log ↑(y / a)) - AnalyticNumberTheory.Sieve.apMiddleLog (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) u v + AnalyticNumberTheory.Sieve.apSmallLog (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) v - distMain (↑y / ↑a) / ↑q.totient

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

The prime-power correction in the exact ψ / log to π conversion.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanSignedCorrectionKernel y a q l = AnalyticNumberTheory.Sieve.apPrimePowerCorrection (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q)

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

Coprime signed main residual. The coprimality condition is deliberately displayed here rather than hidden in the kernel.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanSignedMainSum distMain y X q l f u v = ∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * MathlibNt.SieveTheory.LiuWeight.liuPanSignedMainKernel distMain y a q l u v else 0

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

Coprime signed prime-power correction.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanSignedCorrectionSum y X q l f = ∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * MathlibNt.SieveTheory.LiuWeight.liuPanSignedCorrectionKernel y a q l else 0

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

Nonnegative termwise majorant for the prime-power correction.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanSignedCorrectionBound y X q l f = ∑ a ∈ Finset.Icc 1 X, if a.Coprime q then |f a| * MathlibNt.SieveTheory.LiuWeight.liuPanSignedCorrectionKernel y a q l else 0

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSignedCorrectionBound_nonneg (y X q l : ℕ) (f : ℕ → ℝ) : 0 ≤ liuPanSignedCorrectionBound y X q l f

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeSum_eq_sourceFaithfulSigned (distMain : ℝ → ℝ) (y X q l : ℕ) (f : ℕ → ℝ) (u v : ℕ) (hf0 : f 0 = 0) : liuMainPanCoprimeSum distMain y X q l f = ((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) + liuPanSignedMainSum distMain y X q l f u v - liuPanSignedCorrectionSum y X q l f

Exact finite identity for the arbitrary-main coprime Pan sum. It is constructed from the live Vaughan and Chebyshev identities, not an assumed pointwise split.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanSignedCorrectionSum_le (y X q l : ℕ) (f : ℕ → ℝ) : |liuPanSignedCorrectionSum y X q l f| ≤ liuPanSignedCorrectionBound y X q l f

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuMainPanCoprimeSum_le_sourceFaithfulSigned (distMain : ℝ → ℝ) (y X q l : ℕ) (f : ℕ → ℝ) (u v : ℕ) (hf0 : f 0 = 0) : |liuMainPanCoprimeSum distMain y X q l f| ≤ |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| + (|liuPanSignedMainSum distMain y X q l f u v| + liuPanSignedCorrectionBound y X q l f)

Pointwise absolute-value form of the exact arbitrary-main decomposition.

Canonical residue and source-parameter maxima

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

The double maximum of the concrete signed residual and its separate prime-power correction. For q = 1, its canonical residue is 0.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanSignedResidualMaxY distMain X q x f u v = MathlibNt.SieveTheory.LiuWeight.liuPanScoreMaxY✝ q x fun (y l : ℕ) => |MathlibNt.SieveTheory.LiuWeight.liuPanSignedMainSum distMain y X q l f u v| + MathlibNt.SieveTheory.LiuWeight.liuPanSignedCorrectionBound y X q l f

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSignedResidualMaxY_one (distMain : ℝ → ℝ) (X x : ℕ) (f : ℕ → ℝ) (u v : ℕ) : liuPanSignedResidualMaxY distMain X 1 x f u v = (Finset.image (fun (y : ℕ) => |liuPanSignedMainSum distMain y X 1 0 f u v| + liuPanSignedCorrectionBound y X 1 0 f) (Finset.range (x + 1))).max' ⋯

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

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanMaxY_le_sourceFaithfulSigned (distMain : ℝ → ℝ) (X q x : ℕ) (f : ℕ → ℝ) (u v : ℕ) (hf0 : f 0 = 0) : liuMainPanMaxY distMain X q x f ≤ ((AnalyticNumberTheory.Sieve.panPieceMaxY X q x f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV1 y q l u / Real.log ↑y) + AnalyticNumberTheory.Sieve.panPieceMaxY X q x f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV3 y q l u v / Real.log ↑y) + liuPanSignedResidualMaxY distMain X q x f u v

Maximal pointwise signed decomposition for the arbitrary distribution main.

Uniform source-faithful assembly

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanSourceFaithfulSignedMainBound (distMain : ℝ → ℝ) (x f : ℕ → ℝ) (u v : ℕ) : Prop

The exact inverse-log weighted bound for the concrete arbitrary-main signed residual.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanSourceFaithfulSignedMainBound distMain x f u v = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ) (x₀ : ℕ), ∀ (X : ℕ), x₀ ≤ X → ∑ q ∈ Finset.range (⌊x X ^ (1 / 2) / Real.log (x X) ^ B⌋₊ + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * MathlibNt.SieveTheory.LiuWeight.liuPanSignedResidualMaxY distMain X q ⌊x X⌋₊ f u v ≤ C * x X / Real.log (x X) ^ A

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanMeanValueUniform (distMain : ℝ → ℝ) (x f : ℕ → ℝ) : Prop

The main-parametric analogue of ANT's global Pan mean-value predicate.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanMeanValueUniform distMain x f = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ) (x₀ : ℕ), ∀ (X : ℕ), x₀ ≤ X → ∑ q ∈ Finset.range (⌊x X ^ (1 / 2) / Real.log (x X) ^ B⌋₊ + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * MathlibNt.SieveTheory.LiuWeight.liuMainPanMaxY distMain X q ⌊x X⌋₊ f ≤ C * x X / Real.log (x X) ^ A

theorem MathlibNt.SieveTheory.LiuWeight.LiuMainPanMeanValueUniform.of_sourceFaithfulSignedInputs {distMain : ℝ → ℝ} {x f : ℕ → ℝ} {u v : ℕ} (hI : AnalyticNumberTheory.Sieve.PanTypeICharacterMeanValue x f u) (hII : AnalyticNumberTheory.Sieve.PanTypeIICharacterMeanValue x f u v) (hM : LiuMainPanSourceFaithfulSignedMainBound distMain x f u v) (hfin : AnalyticNumberTheory.Sieve.PanLogEventuallyLarge x) (hf0 : f 0 = 0) : LiuMainPanMeanValueUniform distMain x f

Fixed-source transparent inputs and the Liu endpoint

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

Exact weighted Type I finite input at the source parameter N.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanTypeIPieceBoundAt N f A B C u = ((∑ q ∈ Finset.range (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * AnalyticNumberTheory.Sieve.panPieceMaxY N q N f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV1 y q l u / Real.log ↑y) ≤ C * ↑N / Real.log ↑N ^ A)

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

Exact weighted Type II finite input at the source parameter N.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanTypeIIPieceBoundAt N f A B C u v = ((∑ q ∈ Finset.range (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * AnalyticNumberTheory.Sieve.panPieceMaxY N q N f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV3 y q l u v / Real.log ↑y) ≤ C * ↑N / Real.log ↑N ^ A)

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

Exact weighted finite input for the concrete signed main and prime-power residual at the source parameter N.

Equations

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

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanMeanValueAt_of_concreteSignedInputs (distMain : ℝ → ℝ) (N : ℕ) (f : ℕ → ℝ) (A B C1 C2 C3 : ℝ) (u v : ℕ) (hf0 : f 0 = 0) (hI : LiuMainPanTypeIPieceBoundAt N f A B C1 u) (hII : LiuMainPanTypeIIPieceBoundAt N f A B C2 u v) (hM : LiuMainPanSignedResidualBoundAt distMain N f A B C3 u v) : LiuMainPanMeanValueAt distMain N f A B (C1 + C2 + C3)

The three explicit source-faithful finite inputs produce the fixed-N main-parametric Pan inequality. This does not take a LiuMainPanMeanValueAt witness as an assumption.

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanSourceFamilyInputs (distMain : ℝ → ℝ) (A B C1 C2 C3 : ℝ) (u v : ℕ) : Prop

An eventual family of explicit Type I, Type II, and concrete signed residual inputs for Liu's source-varying weight.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanSourceFamilyInputs distMain A B C1 C2 C3 u v = ∀ᶠ (N : ℕ) in Filter.atTop, MathlibNt.SieveTheory.LiuWeight.LiuMainPanTypeIPieceBoundAt N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) A B C1 u ∧ MathlibNt.SieveTheory.LiuWeight.LiuMainPanTypeIIPieceBoundAt N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) A B C2 u v ∧ MathlibNt.SieveTheory.LiuWeight.LiuMainPanSignedResidualBoundAt distMain N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) A B C3 u v

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuPaperQSourceFullDistributionMajorant_liuLogarithmicIntegral_le_of_sourceFaithfulSignedInputs (κ ε A B C1 C2 C3 : ℝ) (u v : ℕ) (hε : 0 < ε) (hB : 0 ≤ B) (hsource : LiuMainPanSourceFamilyInputs (liuLogarithmicIntegral κ) A B C1 C2 C3 u v) : ∀ᶠ (N : ℕ) in Filter.atTop, liuPaperQSourceFullDistributionMajorant (liuLogarithmicIntegral κ) N ε ≤ (C1 + C2 + C3) * ↑N / Real.log ↑N ^ A + 15 * liuLogarithmicIntegralUpperConstant κ * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2