Character reduction for Liu's aggregate psi term

This module gives exact finite character identities for the aggregate source-convolution psi discrepancy. It separates the principal character before any absolute value or character Cauchy--Schwarz inequality, and then regroups the nonprincipal part by primitive conductor.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanSourceCharacterPrefix (A q : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : ℂ

The source prefix twisted by a Dirichlet character.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanSourceCharacterPrefix A q f χ = ∑ a ∈ Finset.Icc 1 A, ↑(f a) * χ ↑a

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanLambdaCharacterPrefix (t q : ℕ) (χ : DirichletCharacter ℂ q) : ℂ

The von Mangoldt prefix twisted by a Dirichlet character.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanLambdaCharacterPrefix t q χ = ∑ n ∈ Finset.range (t + 1), ↑(ArithmeticFunction.vonMangoldt n) * χ ↑n

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaCharacterPrefix (t q : ℕ) (χ : DirichletCharacter ℂ q) : ℂ

The logarithmically normalized von Mangoldt prefix twisted by a Dirichlet character. The totalized terms at 0 and 1 vanish.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaCharacterPrefix t q χ = ∑ n ∈ Finset.range (t + 1), ↑(ArithmeticFunction.vonMangoldt n / Real.log ↑n) * χ ↑n

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaCharacterPrefix_eq_discreteAbel (t q : ℕ) (χ : DirichletCharacter ℂ q) : liuPanLogLambdaCharacterPrefix t q χ = (↑(Real.log ↑t))⁻¹ * liuPanLambdaCharacterPrefix t q χ + ∑ n ∈ Finset.range t, ↑(liuPanInverseLogAbelWeight n) * liuPanLambdaCharacterPrefix n q χ

Exact discrete Abel summation for a twisted von Mangoldt prefix.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSourceCharacterPrefix_eq_coprime (A q : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : liuPanSourceCharacterPrefix A q f χ = ∑ a ∈ Finset.Icc 1 A, if a.Coprime q then ↑(f a) * χ ↑a else 0

A Dirichlet character kills exactly the nonunit source terms.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAPPsi_complex_eq_characterMean {t q l : ℕ} (hq : 0 < q) (hl : IsUnit ↑l) : ↑(liuPanAPPsi t q l) = (↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q, star (χ ↑l) * liuPanLambdaCharacterPrefix t q χ

Complex character expansion of one complete AP psi sum.

theorem MathlibNt.SieveTheory.LiuWeight.star_dirichletCharacter_natInvMod_mul {q a l : ℕ} (hcop : a.Coprime q) (χ : DirichletCharacter ℂ q) : star (χ ↑(AnalyticNumberTheory.Sieve.natInvMod q a * l % q)) = χ ↑a * star (χ ↑l)

Moving the inverse source residue through conjugation produces the source character and leaves the common residue phase outside.

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

The complex source aggregate before subtracting its uniform main term.

Equations

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

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

The exact all-character mean for the source aggregate. The source prefix and von Mangoldt prefix remain multiplied before any absolute value.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateAPPsiCharacterMean t A q l f = (↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q, star (χ ↑l) * MathlibNt.SieveTheory.LiuWeight.liuPanSourceCharacterPrefix A q f χ * MathlibNt.SieveTheory.LiuWeight.liuPanLambdaCharacterPrefix t q χ

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateAPPsiComplex_eq_characterMean {t A q l : ℕ} (f : ℕ → ℝ) (hq : 0 < q) (hl : IsUnit ↑l) : liuPanAggregateAPPsiComplex t A q l f = liuPanAggregateAPPsiCharacterMean t A q l f

Exact complex character expansion of the source-aggregated AP psi sum.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSourceCharacterPrefix_one_eq_coprime (A q : ℕ) (f : ℕ → ℝ) : liuPanSourceCharacterPrefix A q f 1 = ∑ a ∈ Finset.Icc 1 A, if a.Coprime q then ↑(f a) else 0

The principal source prefix is the source sum restricted to units modulo q; in particular it is not generally the unrestricted source sum.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateAPPsiComplex_eq_real (t A q l : ℕ) (f : ℕ → ℝ) : liuPanAggregateAPPsiComplex t A q l f = ↑(∑ a ∈ Finset.Icc 1 A, if a.Coprime q then f a * liuPanAPPsi t q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) else 0)

Complexification commutes with the source-aggregate AP psi sum.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateAPPsiDiscrepancy_complex_eq (t A q l : ℕ) (f : ℕ → ℝ) : ↑(liuPanAggregateAPPsiDiscrepancy t A q l f) = liuPanAggregateAPPsiComplex t A q l f - liuPanSourceCharacterPrefix A q f 1 * ↑t / ↑q.totient

The real aggregate discrepancy is the complex AP aggregate minus the exact principal source main term.

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

The exact principal-character contribution to the aggregate discrepancy.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePrincipalPsiTerm t A q f = MathlibNt.SieveTheory.LiuWeight.liuPanSourceCharacterPrefix A q f 1 * (MathlibNt.SieveTheory.LiuWeight.liuPanLambdaCharacterPrefix t q 1 - ↑t) / ↑q.totient

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

The exact nonprincipal character contribution, with the source and von Mangoldt prefixes still paired character by character.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateNonprincipalPsiTerm t A q l f = (↑q.totient)⁻¹ * ∑ χ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalCharacters q, star (χ ↑l) * MathlibNt.SieveTheory.LiuWeight.liuPanSourceCharacterPrefix A q f χ * MathlibNt.SieveTheory.LiuWeight.liuPanLambdaCharacterPrefix t q χ

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

The canonical finite character expansion. Modulus zero is assigned zero; the positive-modulus theorem below identifies this with the actual aggregate discrepancy.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePsiCharacterExpansion t A q l f = if q = 0 then 0 else MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePrincipalPsiTerm t A q f + MathlibNt.SieveTheory.LiuWeight.liuPanAggregateNonprincipalPsiTerm t A q l f

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePsiCharacterExpansion_zero (t A l : ℕ) (f : ℕ → ℝ) : liuPanAggregatePsiCharacterExpansion t A 0 l f = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateAPPsiDiscrepancy_complex_eq_characterExpansion {t A q l : ℕ} (f : ℕ → ℝ) (hq : 0 < q) (hl : IsUnit ↑l) : ↑(liuPanAggregateAPPsiDiscrepancy t A q l f) = liuPanAggregatePsiCharacterExpansion t A q l f

Exact principal/nonprincipal character expansion of the aggregate AP psi discrepancy. The principal term is F₁(A) * (Psi₁(t) - t) / phi(q) and is not cancelled.

The exact principal correction

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPsiPrefix (t : ℕ) : ℝ

The ordinary finite Chebyshev psi prefix.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPsiPrefix t = ∑ n ∈ Finset.range (t + 1), ArithmeticFunction.vonMangoldt n

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPsiPrefix_eq_chebyshevPsi (t : ℕ) : liuPanPsiPrefix t = Chebyshev.psi ↑t

The finite psi prefix is exactly Chebyshev's real-variable function at the corresponding natural argument.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPNTError (t : ℕ) : ℝ

The ordinary Chebyshev PNT remainder at a natural argument.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPNTError t = MathlibNt.SieveTheory.LiuWeight.liuPanPsiPrefix t - ↑t

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanLogPNTError (t : ℕ) : ℝ

The totalized inverse-log Abel transform of the ordinary PNT remainder.

Equations

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

theorem MathlibNt.SieveTheory.LiuWeight.eventually_abs_liuPanPNTError_le_mediumPNT : ∃ (c : ℝ), 0 < c ∧ ∃ (C : ℝ), 0 < C ∧ ∃ (N0 : ℕ), ∀ (t : ℕ), N0 ≤ t → |liuPanPNTError t| ≤ C * ↑t * Real.exp (-c * Real.log ↑t ^ (1 / 10))

The medium PNT supplies a natural, pointwise eventual bound for the ordinary psi remainder. The threshold includes all short arguments, where the logarithmic expression need not be used.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_abs_liuPanPNTError_le_div_log_rpow (A : ℝ) (_hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∃ (N0 : ℕ), ∀ (t : ℕ), N0 ≤ t → |liuPanPNTError t| ≤ C * ↑t / Real.log ↑t ^ A

Medium PNT gives every prescribed fixed logarithmic saving for the ordinary natural psi remainder.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanPNTError_le_global_linear (t : ℕ) : |liuPanPNTError t| ≤ (Real.log 4 + 5) * ↑t

A global linear bound for the ordinary PNT remainder, used only to dispose of the finite initial segment in Abel summation.

theorem MathlibNt.SieveTheory.LiuWeight.sum_liuPanInverseLogAbelWeight_le_inv_log_two (t : ℕ) : ∑ n ∈ Finset.range t, liuPanInverseLogAbelWeight n ≤ (Real.log 2)⁻¹

The nonnegative finite Abel weights telescope, uniformly in their upper endpoint.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanInverseLogAbelWeight_le_div_mul_log_sq (n : ℕ) (hn : 2 ≤ n) : liuPanInverseLogAbelWeight n ≤ 1 / (↑n * Real.log ↑n ^ 2)

Away from the totalized exceptional indices, the Abel weight has the expected logarithmic derivative majorant.

theorem MathlibNt.SieveTheory.LiuWeight.sum_Ico_liuPanInverseLogAbelWeight_mul_div_log_pow_le (D L t : ℕ) (hL : 2 ≤ L) : ∑ n ∈ Finset.Ico L t, liuPanInverseLogAbelWeight n * (↑n / Real.log ↑n ^ D) ≤ ↑t / Real.log ↑L ^ (D + 2)

On any tail starting at L ≥ 2, the derivative bound for the Abel weights turns an arbitrary fixed logarithmic PNT majorant into the endpoint scale.

theorem MathlibNt.SieveTheory.LiuWeight.sum_Ico_liuPanInverseLogAbelWeight_mul_absPNTError_le (D L t : ℕ) (C : ℝ) (hL : 2 ≤ L) (hC : 0 ≤ C) (hPNT : ∀ (n : ℕ), L ≤ n → |liuPanPNTError n| ≤ C * ↑n / Real.log ↑n ^ D) : ∑ n ∈ Finset.Ico L t, liuPanInverseLogAbelWeight n * |liuPanPNTError n| ≤ C * ↑t / Real.log ↑L ^ (D + 2)

A pointwise logarithmic PNT majorant transfers through any Abel tail with the two extra logarithms supplied by the derivative of the Abel weight.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanLogPNTError_le_global_linear (t : ℕ) : |liuPanLogPNTError t| ≤ 2 * (Real.log 4 + 5) * (Real.log 2)⁻¹ * ↑t

The totalized Abel transform of the PNT error has a global linear majorant. This is the short-range input for the logarithmically saving tail estimate.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_abs_liuPanLogPNTError_le_div_log_pow (A : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∃ (N0 : ℕ), ∀ (t : ℕ), N0 ≤ t → |liuPanLogPNTError t| ≤ C * ↑t / Real.log ↑t ^ A

Every fixed natural logarithmic saving eventually holds for the totalized inverse-log Abel transform of the ordinary PNT remainder.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_abs_liuPanLogPNTError_le_div_log_rpow (A : ℝ) (_hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∃ (N0 : ℕ), ∀ (t : ℕ), N0 ≤ t → |liuPanLogPNTError t| ≤ C * ↑t / Real.log ↑t ^ A

Every fixed positive real logarithmic saving eventually holds for the totalized inverse-log Abel transform of the ordinary PNT remainder.

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLogPNTError_zero : liuPanLogPNTError 0 = 0

Totalized inverse-log Abel weights remove the exceptional argument zero.

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLogPNTError_one : liuPanLogPNTError 1 = 0

Totalized inverse-log Abel weights remove the exceptional argument one.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPsiNoncoprimeCorrection (t q : ℕ) : ℝ

The part of psi supported on integers not coprime to the modulus. Since von Mangoldt is supported on prime powers, these are exactly the prime-power terms whose prime divides q.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPsiNoncoprimeCorrection t q = ∑ n ∈ Finset.range (t + 1), if n.Coprime q then 0 else ArithmeticFunction.vonMangoldt n

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanLogNoncoprimeCorrection (t q : ℕ) : ℝ

The logarithmically normalized noncoprime prime-power correction. The terms at 0 and 1 vanish, so this is a total finite sum.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanLogNoncoprimeCorrection t q = ∑ n ∈ Finset.range (t + 1), if n.Coprime q then 0 else ArithmeticFunction.vonMangoldt n / Real.log ↑n

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLogNoncoprimeCorrection_eq_discreteAbel (t q : ℕ) : liuPanLogNoncoprimeCorrection t q = (Real.log ↑t)⁻¹ * liuPanPsiNoncoprimeCorrection t q + ∑ n ∈ Finset.range t, liuPanInverseLogAbelWeight n * liuPanPsiNoncoprimeCorrection n q

Discrete Abel summation for the noncoprime prime-power correction.

def MathlibNt.SieveTheory.LiuWeight.liuPanNoncoprimePrimePowerCount (t q : ℕ) : ℕ

The finite number of relevant prime powers: exactly those whose prime divides the modulus, expressed without choosing that prime.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanNoncoprimePrimePowerCount t q = {n ∈ Finset.range (t + 1) | ¬n.Coprime q ∧ IsPrimePow n}.card

theorem MathlibNt.SieveTheory.LiuWeight.liuPanNoncoprimePrimePowerCount_le_primeFactors_mul_log (N t q : ℕ) (ht : t ≤ N) (hq : q ≠ 0) : liuPanNoncoprimePrimePowerCount t q ≤ q.primeFactors.card * (1 + Nat.log 2 N)

A noncoprime prime power is determined by its unique base prime dividing the positive modulus and an exponent at most log₂ N.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLogNoncoprimeCorrection_eq_sum_primePowers (t q : ℕ) : liuPanLogNoncoprimeCorrection t q = ∑ n ∈ Finset.range (t + 1) with ¬n.Coprime q ∧ IsPrimePow n, ArithmeticFunction.vonMangoldt n / Real.log ↑n

Prime-power support of von Mangoldt localizes the logarithmic correction to the displayed finite count.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLogNoncoprimeCorrection_le_primePowerCount (t q : ℕ) : liuPanLogNoncoprimeCorrection t q ≤ ↑(liuPanNoncoprimePrimePowerCount t q)

Each logarithmically normalized von Mangoldt term on prime-power support is at most one.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanNoncoprimePrimePowerCountMax (N q : ℕ) : ℝ

The largest prime-power count needed by source quotients with y ≤ N.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanNoncoprimePrimePowerCountMax N q = (Finset.image (fun (t : ℕ) => ↑(MathlibNt.SieveTheory.LiuWeight.liuPanNoncoprimePrimePowerCount t q)) (Finset.range (N + 1))).max' ⋯

theorem MathlibNt.SieveTheory.LiuWeight.liuPanNoncoprimePrimePowerCountMax_le_primeFactors_mul_log (N q : ℕ) (hq : q ≠ 0) : liuPanNoncoprimePrimePowerCountMax N q ≤ ↑(q.primeFactors.card * (1 + Nat.log 2 N))

The same prime-factor/exponent count controls every prefix up to N.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanNoncoprimePrimePowerCountMax_le_log_sq (N q : ℕ) (hN : 3 ≤ N) (hq : 0 < q) (hqN : q ≤ N) : liuPanNoncoprimePrimePowerCountMax N q ≤ 1 / Real.log 2 * (1 + 1 / Real.log 2) * Real.log ↑N ^ 2

Uniformly for positive q ≤ N, the finite prime-power count costs only two logarithms.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanNoncoprimePrimePowerCount_le_max {N t q : ℕ} (ht : t ≤ N) : ↑(liuPanNoncoprimePrimePowerCount t q) ≤ liuPanNoncoprimePrimePowerCountMax N q

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLogNoncoprimeCorrection_le_primePowerCountMax {N t q : ℕ} (ht : t ≤ N) : liuPanLogNoncoprimeCorrection t q ≤ liuPanNoncoprimePrimePowerCountMax N q

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLogNoncoprimeCorrection_one (t : ℕ) : liuPanLogNoncoprimeCorrection t 1 = 0

Modulus one has no noncoprime prime-power correction.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLambdaCharacterPrefix_one_eq_psi_sub_noncoprime (t q : ℕ) : liuPanLambdaCharacterPrefix t q 1 = ↑(liuPanPsiPrefix t) - ↑(liuPanPsiNoncoprimeCorrection t q)

The principal character selects psi minus the noncoprime prime-power correction.

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

The ordinary PNT-error part of the principal character contribution.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePrincipalPNTTerm t A q f = MathlibNt.SieveTheory.LiuWeight.liuPanSourceCharacterPrefix A q f 1 * (↑(MathlibNt.SieveTheory.LiuWeight.liuPanPsiPrefix t) - ↑t) / ↑q.totient

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

The real source aggregate paired with the ordinary PNT remainder.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePNTError t A q f = (∑ a ∈ Finset.Icc 1 A, if a.Coprime q then f a else 0) * MathlibNt.SieveTheory.LiuWeight.liuPanPNTError t

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePrincipalPNTTerm_eq_real (t A q : ℕ) (f : ℕ → ℝ) : liuPanAggregatePrincipalPNTTerm t A q f = ↑(liuPanAggregatePNTError t A q f) / ↑q.totient

The complex principal PNT term is the complexification of its real source aggregate, followed by the totient normalization.

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

The correction to the principal term from prime powers whose prime divides the modulus.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePrincipalNoncoprimePsiTerm t A q f = MathlibNt.SieveTheory.LiuWeight.liuPanSourceCharacterPrefix A q f 1 * ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPsiNoncoprimeCorrection t q) / ↑q.totient

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

The real source aggregate paired with the noncoprime psi correction.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateNoncoprimePsiCorrection t A q f = (∑ a ∈ Finset.Icc 1 A, if a.Coprime q then f a else 0) * MathlibNt.SieveTheory.LiuWeight.liuPanPsiNoncoprimeCorrection t q

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePrincipalNoncoprimePsiTerm_eq_real (t A q : ℕ) (f : ℕ → ℝ) : liuPanAggregatePrincipalNoncoprimePsiTerm t A q f = ↑(liuPanAggregateNoncoprimePsiCorrection t A q f) / ↑q.totient

The complex principal correction is just the complexification of its real source aggregate, followed by the totient normalization.

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePrincipalNoncoprimePsiTerm_zero (t A : ℕ) (f : ℕ → ℝ) : liuPanAggregatePrincipalNoncoprimePsiTerm t A 0 f = 0

The zero modulus is canonically killed by the totient normalization.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateNoncoprimePsiCorrection_endpoint_shell (y X q : ℕ) (f g : ℕ → ℝ) (hg0 : g 0 = 0) : (∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * g (y / a) * liuPanPsiNoncoprimeCorrection (y / a) q else 0) = ∑ k ∈ Finset.Icc 1 y, g k * (liuPanAggregateNoncoprimePsiCorrection k (liuPanAbelSourceCutoff y X k) q f - liuPanAggregateNoncoprimePsiCorrection k (liuPanAbelSourceCutoff y X (k + 1)) q f)

The source-aggregated endpoint shell for a scalar noncoprime correction.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateNoncoprimePsiCorrection_prefix_swap (y X q : ℕ) (f w : ℕ → ℝ) : (∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * ∑ n ∈ Finset.range (y / a), w n * liuPanPsiNoncoprimeCorrection n q else 0) = ∑ n ∈ Finset.range y, w n * liuPanAggregateNoncoprimePsiCorrection n (liuPanAbelSourceCutoff y X (n + 1)) q f

Swapping the source sum with scalar noncoprime correction prefixes retains the shared Abel source cutoff.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePrincipalPsiTerm_eq_pnt_sub_noncoprime (t A q : ℕ) (f : ℕ → ℝ) : liuPanAggregatePrincipalPsiTerm t A q f = liuPanAggregatePrincipalPNTTerm t A q f - liuPanAggregatePrincipalNoncoprimePsiTerm t A q f

Exact principal split into the ordinary PNT error and the modulus- noncoprime correction.

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalCharacters_one : liuPanPrimePowerNonprincipalCharacters 1 = ∅

At modulus one there are no nonprincipal characters.

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateNonprincipalPsiTerm_one (t A l : ℕ) (f : ℕ → ℝ) : liuPanAggregateNonprincipalPsiTerm t A 1 l f = 0

Modulus one consists only of the principal psi contribution.

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePsiCharacterExpansion_one (t A l : ℕ) (f : ℕ → ℝ) : liuPanAggregatePsiCharacterExpansion t A 1 l f = liuPanAggregatePrincipalPsiTerm t A 1 f

At modulus one the canonical expansion is principal only.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateAPPsiDiscrepancy_complex_one (t A l : ℕ) (f : ℕ → ℝ) : ↑(liuPanAggregateAPPsiDiscrepancy t A 1 l f) = liuPanAggregatePrincipalPsiTerm t A 1 f

The actual aggregate discrepancy at modulus one is principal only.

Primitive dilation on the source and von Mangoldt sides

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanSourceZeroExtension (f : ℕ → ℝ) (a : ℕ) : ℂ

The source sequence extended by zero at the excluded index 0.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanSourceZeroExtension f a = if a = 0 then 0 else ↑(f a)

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSourceCharacterPrefix_eq_zeroExtension (A q : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : liuPanSourceCharacterPrefix A q f χ = ∑ a ∈ Finset.range (A + 1), liuPanSourceZeroExtension f a * χ ↑a

The source prefix as a zero-extended range sum, in the form consumed by the generic induced-character dilation identity.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSourceCharacterPrefix_eq_primitive_dilations {q : ℕ} [NeZero q] (A : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : liuPanSourceCharacterPrefix A q f χ = ∑ e ∈ (q / χ.conductor).divisors, ↑(ArithmeticFunction.moebius e) * χ.primitiveCharacter ↑e * ∑ m ∈ Finset.range (A / e + 1), liuPanSourceZeroExtension f (e * m) * χ.primitiveCharacter ↑m

Exact conductor-first primitive/Möbius-dilation transfer of the source prefix for one induced character.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLambdaCharacterPrefix_eq_primitive_dilations {q : ℕ} [NeZero q] (t : ℕ) (χ : DirichletCharacter ℂ q) : liuPanLambdaCharacterPrefix t q χ = ∑ e ∈ (q / χ.conductor).divisors, ↑(ArithmeticFunction.moebius e) * χ.primitiveCharacter ↑e * ∑ m ∈ Finset.range (t / e + 1), ↑(ArithmeticFunction.vonMangoldt (e * m)) * χ.primitiveCharacter ↑m

Exact conductor-first primitive/Möbius-dilation transfer of the von Mangoldt prefix for one induced character.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSource_mul_lambda_eq_primitive_dilations {q : ℕ} [NeZero q] (t A : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : liuPanSourceCharacterPrefix A q f χ * liuPanLambdaCharacterPrefix t q χ = (∑ e ∈ (q / χ.conductor).divisors, ↑(ArithmeticFunction.moebius e) * χ.primitiveCharacter ↑e * ∑ m ∈ Finset.range (A / e + 1), liuPanSourceZeroExtension f (e * m) * χ.primitiveCharacter ↑m) * ∑ e ∈ (q / χ.conductor).divisors, ↑(ArithmeticFunction.moebius e) * χ.primitiveCharacter ↑e * ∑ m ∈ Finset.range (t / e + 1), ↑(ArithmeticFunction.vonMangoldt (e * m)) * χ.primitiveCharacter ↑m

Both factors of the aggregate character product transfer to primitive dilations before any absolute value or character Cauchy--Schwarz step.

Exact conductor-first regrouping

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePsiCharacterProduct (t A q l : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : ℂ

The nonprincipal character product at one level.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePsiCharacterProduct t A q l f χ = star (χ ↑l) * MathlibNt.SieveTheory.LiuWeight.liuPanSourceCharacterPrefix A q f χ * MathlibNt.SieveTheory.LiuWeight.liuPanLambdaCharacterPrefix t q χ

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

The nonprincipal sum regrouped by exact conductor. Conductor one is absent from the indexing interval.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePsiConductorSum t A q l f = (↑q.totient)⁻¹ * ∑ d ∈ Finset.Icc 2 q, ∑ χ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalCharacters q with χ.conductor = d, MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePsiCharacterProduct t A q l f χ

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePsiConductorSum_zero (t A l : ℕ) (f : ℕ → ℝ) : liuPanAggregatePsiConductorSum t A 0 l f = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePsiConductorSum_one (t A l : ℕ) (f : ℕ → ℝ) : liuPanAggregatePsiConductorSum t A 1 l f = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateNonprincipalPsiTerm_eq_conductorSum {t A q l : ℕ} (f : ℕ → ℝ) (hq : 0 < q) : liuPanAggregateNonprincipalPsiTerm t A q l f = liuPanAggregatePsiConductorSum t A q l f

Exact regrouping of the nonprincipal aggregate by conductor, before any absolute value or Cauchy--Schwarz inequality.

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

The conductor sum reindexed by the unique primitive character inducing each nonprincipal character.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePsiPrimitiveLiftSum t A q l f = (↑q.totient)⁻¹ * ∑ d ∈ Finset.Icc 2 q, if hdq : d ∣ q then ∑ ψ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters d, MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePsiCharacterProduct t A q l f ((DirichletCharacter.changeLevel hdq) ψ) else 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePsiPrimitiveLiftSum_zero (t A l : ℕ) (f : ℕ → ℝ) : liuPanAggregatePsiPrimitiveLiftSum t A 0 l f = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePsiPrimitiveLiftSum_one (t A l : ℕ) (f : ℕ → ℝ) : liuPanAggregatePsiPrimitiveLiftSum t A 1 l f = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePsiConductorSum_eq_primitiveLiftSum {t A q l : ℕ} (f : ℕ → ℝ) (hq : 0 < q) : liuPanAggregatePsiConductorSum t A q l f = liuPanAggregatePsiPrimitiveLiftSum t A q l f

Exact primitive-character reindexing of the conductor-first aggregate.

Substitution into the aggregate Abel term

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

The exact character expansion substituted into both shared-y Abel sums.

Equations

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

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPsiCharacterTerm_zero (y X l : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogPsiCharacterTerm y X 0 l f = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPsiTerm_complex_eq_characterTerm {y X q l : ℕ} (f : ℕ → ℝ) (hq : 0 < q) (hl : IsUnit ↑l) : ↑(liuPanAggregateInverseLogPsiTerm y X q l f) = liuPanAggregateInverseLogPsiCharacterTerm y X q l f

Exact substitution into liuPanAggregateInverseLogPsiTerm; all source cutoffs, shell differences, and common y parameters are unchanged.

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

The principal contribution after substitution into the shared-y Abel shell and prefix sums.

Equations

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

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

The ordinary PNT-error part of the principal shared-y Abel term.

Equations

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

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

The real shared-y Abel aggregation of the ordinary PNT remainder.

Equations

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

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePNTError_endpoint_shell (y X q : ℕ) (f g : ℕ → ℝ) (hg0 : g 0 = 0) : (∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * g (y / a) * liuPanPNTError (y / a) else 0) = ∑ k ∈ Finset.Icc 1 y, g k * (liuPanAggregatePNTError k (liuPanAbelSourceCutoff y X k) q f - liuPanAggregatePNTError k (liuPanAbelSourceCutoff y X (k + 1)) q f)

The source-aggregated endpoint shell for the scalar ordinary PNT remainder.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregatePNTError_prefix_swap (y X q : ℕ) (f w : ℕ → ℝ) : (∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * ∑ n ∈ Finset.range (y / a), w n * liuPanPNTError n else 0) = ∑ n ∈ Finset.range y, w n * liuPanAggregatePNTError n (liuPanAbelSourceCutoff y X (n + 1)) q f

Swapping source summation with ordinary PNT prefixes retains the shared Abel source cutoff.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPNTError_eq_source (y X q : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogPNTError y X q f = ∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * liuPanLogPNTError (y / a) else 0

The ordinary PNT Abel aggregate is exactly the source convolution with the totalized inverse-log PNT remainder.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPrincipalPNTTerm_eq_real (y X q : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogPrincipalPNTTerm y X q f = ↑(liuPanAggregateInverseLogPNTError y X q f) / ↑q.totient

Complexification and the totient factor commute with the complete ordinary-PNT shared-y Abel aggregation.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPrincipalPNTTerm_eq_source (y X q : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogPrincipalPNTTerm y X q f = ↑(∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * liuPanLogPNTError (y / a) else 0) / ↑q.totient

Exact real source form of the ordinary principal/PNT term. In particular, the same y / a quotient remains inside the totalized Abel remainder.

theorem MathlibNt.SieveTheory.LiuWeight.liuWeight_le_one (N z y a : ℕ) : liuWeight N z y a ≤ 1

The exact Liu source is an indicator, so replacing it by one is permitted only through this explicit pointwise upper bound.

theorem MathlibNt.SieveTheory.LiuWeight.sum_liuWeight_div_le_liuHarmonic (N : ℕ) : ∑ a ∈ Finset.Icc 1 N, liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a / ↑a ≤ liuHarmonic N

The reciprocal mass of the actual Liu source is bounded by the harmonic sum; this is the source factor used for the long-quotient PNT range.

theorem MathlibNt.SieveTheory.LiuWeight.sum_liuWeight_div_le_one_add_log (N : ℕ) : ∑ a ∈ Finset.Icc 1 N, liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a / ↑a ≤ 1 + Real.log ↑N

The reciprocal Liu-source mass costs at most one logarithm.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanPrincipalPNTSourceSum_le_global (N y q : ℕ) : |∑ a ∈ Finset.Icc 1 N, if a.Coprime q then liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a * liuPanLogPNTError (y / a) else 0| ≤ 2 * (Real.log 4 + 5) * (Real.log 2)⁻¹ * ↑y * (1 + Real.log ↑N)

The global linear Abel bound, summed against the reciprocal Liu source. This is the short-y input in the principal source-family estimate.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuWeight_quotient_ge_rpow_one_ninth : ∃ (N0 : ℕ), ∀ (N : ℕ), N0 ≤ N → ∀ (y : ℕ), ↑N ^ (5 / 6) ≤ ↑y → ∀ a ∈ Finset.Icc 1 N, liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a ≠ 0 → ↑N ^ (1 / 9) ≤ ↑(y / a)

Once y reaches the five-sixths scale, every nonzero Liu source produces a quotient at least at the one-ninth scale. The weaker exponent absorbs the integer division uniformly.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanPrincipalPNTSourceSum_le_large (D C : ℝ) (hD : 0 < D) (hC : 0 ≤ C) (T0 : ℕ) (hscalar : ∀ (t : ℕ), T0 ≤ t → |liuPanLogPNTError t| ≤ C * ↑t / Real.log ↑t ^ D) {N y q : ℕ} (hN : 3 ≤ N) (hT0 : ↑T0 ≤ ↑N ^ (1 / 9)) (hquot : ∀ a ∈ Finset.Icc 1 N, liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a ≠ 0 → ↑N ^ (1 / 9) ≤ ↑(y / a)) : |∑ a ∈ Finset.Icc 1 N, if a.Coprime q then liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a * liuPanLogPNTError (y / a) else 0| ≤ C * 9 ^ D * ↑y / Real.log ↑N ^ D * (1 + Real.log ↑N)

On the large-y range, a scalar logarithmic PNT bound may be applied uniformly to every nonzero Liu source quotient.

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

The modulus-noncoprime correction in the same shared-y Abel shell and prefix aggregation.

Equations

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

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

The real shared-y Abel aggregation of the noncoprime correction.

Equations

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

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNoncoprimeCorrection_eq_source (y X q : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogNoncoprimeCorrection y X q f = ∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * liuPanLogNoncoprimeCorrection (y / a) q else 0

The aggregate correction is exactly the source sum of the logarithmically normalized noncoprime prime-power correction; the same shared y and source cutoffs are retained.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPrincipalNoncoprimePsiTerm_eq_real (y X q : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogPrincipalNoncoprimePsiTerm y X q f = ↑(liuPanAggregateInverseLogNoncoprimeCorrection y X q f) / ↑q.totient

Complexification and the totient factor commute with the complete shared-y noncoprime Abel aggregation.

@[simp]

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

The shared-y principal noncoprime term also vanishes canonically at modulus zero.

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNoncoprimeCorrection_one (y X : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogNoncoprimeCorrection y X 1 f = 0

At modulus one the source form is exactly zero, not merely bounded.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNoncoprimeCorrection_source_le (N y q : ℕ) (hy : y ≤ N) (hN : 1 ≤ N) : liuPanAggregateInverseLogNoncoprimeCorrection y N q (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) ≤ 3 * ↑N ^ (2 / 3) * liuPanNoncoprimePrimePowerCountMax N q

Product-cube source support gives the exact N^(2/3) factor in the noncoprime correction. The remaining factor is only the finite count of prime powers at primes dividing the modulus.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNoncoprimeCorrectionMaxY (N q : ℕ) : ℝ

Canonical maximum of the real noncoprime correction over the shared parameter y ≤ N.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNoncoprimeCorrectionMaxY N q = (Finset.image (fun (y : ℕ) => MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNoncoprimeCorrection y N q (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N))) (Finset.range (N + 1))).max' ⋯

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNoncoprimeCorrectionMaxY_source_le (N q : ℕ) (hN : 1 ≤ N) : liuPanAggregateInverseLogNoncoprimeCorrectionMaxY N q ≤ 3 * ↑N ^ (2 / 3) * liuPanNoncoprimePrimePowerCountMax N q

The source-support bound is uniform through the canonical y maximum.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanNoncoprimePrimePowerCountMaxModulus (N Q : ℕ) : ℝ

A uniform finite prime-power count over moduli up to Q.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanNoncoprimePrimePowerCountMaxModulus N Q = (Finset.image (fun (q : ℕ) => MathlibNt.SieveTheory.LiuWeight.liuPanNoncoprimePrimePowerCountMax N q) (Finset.range (Q + 1))).max' ⋯

theorem MathlibNt.SieveTheory.LiuWeight.liuPanNoncoprimePrimePowerCountMax_le_maxModulus {N Q q : ℕ} (hq : q ≤ Q) : liuPanNoncoprimePrimePowerCountMax N q ≤ liuPanNoncoprimePrimePowerCountMaxModulus N Q

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

The modulus-weighted noncoprime correction average; its weight is precisely the squarefree weight used by H₃.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateInverseLogNoncoprimeCorrectionAverage N B = ∑ q ∈ Finset.range (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B + 1), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight q * (MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNoncoprimeCorrectionMaxY N q / ↑q.totient)

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateInverseLogNoncoprimeCorrectionAverage_source_le (N : ℕ) (B : ℝ) (hN : 1 ≤ N) : liuMainPanAggregateInverseLogNoncoprimeCorrectionAverage N B ≤ 3 * ↑N ^ (2 / 3) * liuPanNoncoprimePrimePowerCountMaxModulus N (panModulusCutoff N B) * liuPanPrimePowerH3Mass (panModulusCutoff N B)

Lifting the source estimate through the squarefree modulus average costs exactly H₃; no full-psi or square-root correction is introduced.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateInverseLogNoncoprimeCorrectionAverage_source_le_log_sq (N : ℕ) (B : ℝ) (hN : 3 ≤ N) (hB : 0 ≤ B) : liuMainPanAggregateInverseLogNoncoprimeCorrectionAverage N B ≤ 3 * ↑N ^ (2 / 3) * (1 / Real.log 2 * (1 + 1 / Real.log 2) * Real.log ↑N ^ 2) * liuPanPrimePowerH3Mass (panModulusCutoff N B)

The sharp prime-factor/exponent count removes the auxiliary maximum: uniformly in B ≥ 0, only two logarithms remain before the H₃ mass.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateInverseLogNoncoprimeCorrectionAverage_le_rpow_polylog : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ) (B : ℝ), 3 ≤ N → 0 ≤ B → liuMainPanAggregateInverseLogNoncoprimeCorrectionAverage N B ≤ C * ↑N ^ (2 / 3) * Real.log ↑N ^ 8

The modulus-noncoprime correction has the unconditional N^(2/3) log(N)^8 scale, uniformly in the Pan parameter B ≥ 0.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuMainPanAggregateInverseLogNoncoprimeCorrectionAverage_le (A : ℝ) (_hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∃ (N0 : ℕ), ∀ (N : ℕ), N0 ≤ N → ∀ (B : ℝ), 0 ≤ B → liuMainPanAggregateInverseLogNoncoprimeCorrectionAverage N B ≤ C * ↑N / Real.log ↑N ^ A

Every fixed logarithmic saving eventually dominates the unconditional noncoprime correction, uniformly for all B ≥ 0.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPrincipalPsiTerm_eq_pnt_sub_noncoprime (y X q : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogPrincipalPsiTerm y X q f = liuPanAggregateInverseLogPrincipalPNTTerm y X q f - liuPanAggregateInverseLogPrincipalNoncoprimePsiTerm y X q f

The exact principal Abel term is ordinary PNT error minus the noncoprime prime-power correction. The source cutoffs and the common y are unchanged.

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

The nonprincipal contribution after substitution into the same Abel shell and prefix sums.

Equations

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

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNonprincipalPsiTerm_zero (y X l : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogNonprincipalPsiTerm y X 0 l f = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNonprincipalPsiTerm_one (y X l : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogNonprincipalPsiTerm y X 1 l f = 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanSourceLogLambdaCharacterHyperbola (y X q : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : ℂ

One character's exact inverse-log hyperbola convolution. The source and von Mangoldt factors remain paired before any norm is taken.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanSourceLogLambdaCharacterHyperbola y X q f χ = ∑ a ∈ Finset.Icc 1 X, ↑(f a) * χ ↑a * MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaCharacterPrefix (y / a) q χ

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSourceLogLambdaCharacterHyperbola_eq_abel (y X q : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : liuPanSourceLogLambdaCharacterHyperbola y X q f χ = ∑ k ∈ Finset.Icc 1 y, (↑(Real.log ↑k))⁻¹ * (liuPanSourceCharacterPrefix (liuPanAbelSourceCutoff y X k) q f χ * liuPanLambdaCharacterPrefix k q χ - liuPanSourceCharacterPrefix (liuPanAbelSourceCutoff y X (k + 1)) q f χ * liuPanLambdaCharacterPrefix k q χ) + ∑ n ∈ Finset.range y, ↑(liuPanInverseLogAbelWeight n) * (liuPanSourceCharacterPrefix (liuPanAbelSourceCutoff y X (n + 1)) q f χ * liuPanLambdaCharacterPrefix n q χ)

For one character, the shared-y Abel shell is exactly the original source/Lambda hyperbola convolution.

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

The nonprincipal inverse-log term in its exact character-by-character hyperbola form. Modulus zero is assigned zero canonically.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateNonprincipalLogLambdaHyperbola y X q l f = if q = 0 then 0 else (↑q.totient)⁻¹ * ∑ χ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalCharacters q, star (χ ↑l) * MathlibNt.SieveTheory.LiuWeight.liuPanSourceLogLambdaCharacterHyperbola y X q f χ

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateNonprincipalLogLambdaHyperbola_zero (y X l : ℕ) (f : ℕ → ℝ) : liuPanAggregateNonprincipalLogLambdaHyperbola y X 0 l f = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateNonprincipalLogLambdaHyperbola_one (y X l : ℕ) (f : ℕ → ℝ) : liuPanAggregateNonprincipalLogLambdaHyperbola y X 1 l f = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNonprincipalPsiTerm_eq_logLambdaHyperbola {y X q l : ℕ} (f : ℕ → ℝ) (hq : 0 < q) : liuPanAggregateInverseLogNonprincipalPsiTerm y X q l f = liuPanAggregateNonprincipalLogLambdaHyperbola y X q l f

Exact pre-norm hyperbola identity for the nonprincipal part of the aggregate inverse-log discrepancy. The source coefficient and Lambda prefix stay coupled inside each character summand.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNonprincipalPsiTerm_eq_character_hyperbola {y X q l : ℕ} (f : ℕ → ℝ) (hq : 0 < q) : liuPanAggregateInverseLogNonprincipalPsiTerm y X q l f = (↑q.totient)⁻¹ * ∑ χ ∈ liuPanPrimePowerNonprincipalCharacters q, star (χ ↑l) * ∑ a ∈ Finset.Icc 1 X, ↑(f a) * χ ↑a * ∑ m ∈ Finset.range (y / a + 1), ↑(ArithmeticFunction.vonMangoldt m / Real.log ↑m) * χ ↑m

Expanded form of the nonprincipal hyperbola identity, displaying both finite source and Lambda sums explicitly.

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

The logarithmic hyperbola sum regrouped by exact conductor.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaConductorSum y X q l f = if q = 0 then 0 else (↑q.totient)⁻¹ * ∑ d ∈ Finset.Icc 2 q, ∑ χ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalCharacters q with χ.conductor = d, star (χ ↑l) * MathlibNt.SieveTheory.LiuWeight.liuPanSourceLogLambdaCharacterHyperbola y X q f χ

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaConductorSum_zero (y X l : ℕ) (f : ℕ → ℝ) : liuPanAggregateLogLambdaConductorSum y X 0 l f = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaConductorSum_one (y X l : ℕ) (f : ℕ → ℝ) : liuPanAggregateLogLambdaConductorSum y X 1 l f = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateNonprincipalLogLambdaHyperbola_eq_conductorSum {y X q l : ℕ} (f : ℕ → ℝ) (hq : 0 < q) : liuPanAggregateNonprincipalLogLambdaHyperbola y X q l f = liuPanAggregateLogLambdaConductorSum y X q l f

Regrouping the logarithmic hyperbola by conductor is exact and precedes every norm or Cauchy--Schwarz inequality.

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

The conductor-grouped logarithmic hyperbola reindexed by primitive characters and their unique lifts to level q.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaPrimitiveLiftSum y X q l f = if q = 0 then 0 else (↑q.totient)⁻¹ * ∑ d ∈ Finset.Icc 2 q, if hdq : d ∣ q then ∑ ψ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters d, star (((DirichletCharacter.changeLevel hdq) ψ) ↑l) * MathlibNt.SieveTheory.LiuWeight.liuPanSourceLogLambdaCharacterHyperbola y X q f ((DirichletCharacter.changeLevel hdq) ψ) else 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaPrimitiveLiftSum_zero (y X l : ℕ) (f : ℕ → ℝ) : liuPanAggregateLogLambdaPrimitiveLiftSum y X 0 l f = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaPrimitiveLiftSum_one (y X l : ℕ) (f : ℕ → ℝ) : liuPanAggregateLogLambdaPrimitiveLiftSum y X 1 l f = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaConductorSum_eq_primitiveLiftSum {y X q l : ℕ} (f : ℕ → ℝ) (hq : 0 < q) : liuPanAggregateLogLambdaConductorSum y X q l f = liuPanAggregateLogLambdaPrimitiveLiftSum y X q l f

Exact primitive-character reindexing of the logarithmic hyperbola.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorSum (D₀ y X q l : ℕ) (f : ℕ → ℝ) : ℂ

Primitive conductors at most D₀, retained in their exact lifted hyperbola form.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorSum D₀ y X q l f = if q = 0 then 0 else (↑q.totient)⁻¹ * ∑ d ∈ Finset.Icc 2 q, if d ≤ D₀ then if hdq : d ∣ q then ∑ ψ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters d, star (((DirichletCharacter.changeLevel hdq) ψ) ↑l) * MathlibNt.SieveTheory.LiuWeight.liuPanSourceLogLambdaCharacterHyperbola y X q f ((DirichletCharacter.changeLevel hdq) ψ) else 0 else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaMediumHighConductorSum (D₀ y X q l : ℕ) (f : ℕ → ℝ) : ℂ

Primitive conductors above D₀, the medium/high bilinear family.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaMediumHighConductorSum D₀ y X q l f = if q = 0 then 0 else (↑q.totient)⁻¹ * ∑ d ∈ Finset.Icc 2 q, if D₀ < d then if hdq : d ∣ q then ∑ ψ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters d, star (((DirichletCharacter.changeLevel hdq) ψ) ↑l) * MathlibNt.SieveTheory.LiuWeight.liuPanSourceLogLambdaCharacterHyperbola y X q f ((DirichletCharacter.changeLevel hdq) ψ) else 0 else 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorSum_zero (D₀ y X l : ℕ) (f : ℕ → ℝ) : liuPanAggregateLogLambdaLowConductorSum D₀ y X 0 l f = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaMediumHighConductorSum_zero (D₀ y X l : ℕ) (f : ℕ → ℝ) : liuPanAggregateLogLambdaMediumHighConductorSum D₀ y X 0 l f = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorSum_one (D₀ y X l : ℕ) (f : ℕ → ℝ) : liuPanAggregateLogLambdaLowConductorSum D₀ y X 1 l f = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaMediumHighConductorSum_one (D₀ y X l : ℕ) (f : ℕ → ℝ) : liuPanAggregateLogLambdaMediumHighConductorSum D₀ y X 1 l f = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaPrimitiveLiftSum_eq_low_add_mediumHigh {y X q l : ℕ} (D₀ : ℕ) (f : ℕ → ℝ) (hq : 0 < q) : liuPanAggregateLogLambdaPrimitiveLiftSum y X q l f = liuPanAggregateLogLambdaLowConductorSum D₀ y X q l f + liuPanAggregateLogLambdaMediumHighConductorSum D₀ y X q l f

Exact low/medium-high conductor partition at an arbitrary threshold D₀.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNonprincipalPsiTerm_eq_low_add_mediumHigh {y X q l : ℕ} (D₀ : ℕ) (f : ℕ → ℝ) (hq : 0 < q) : liuPanAggregateInverseLogNonprincipalPsiTerm y X q l f = liuPanAggregateLogLambdaLowConductorSum D₀ y X q l f + liuPanAggregateLogLambdaMediumHighConductorSum D₀ y X q l f

The nonprincipal Abel term is exactly the low-conductor plus medium/high primitive hyperbola families.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPsiCharacterTerm_eq_principal_add_nonprincipal {y X q l : ℕ} (f : ℕ → ℝ) (hq : 0 < q) : liuPanAggregateInverseLogPsiCharacterTerm y X q l f = liuPanAggregateInverseLogPrincipalPsiTerm y X q f + liuPanAggregateInverseLogNonprincipalPsiTerm y X q l f

The substituted Abel term splits exactly into principal and nonprincipal parts, still before taking an absolute value.

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPsiCharacterTerm_one (y X l : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogPsiCharacterTerm y X 1 l f = liuPanAggregateInverseLogPrincipalPsiTerm y X 1 f

At modulus one the substituted Abel character term is principal only.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPsiTerm_complex_one (y X l : ℕ) (f : ℕ → ℝ) : ↑(liuPanAggregateInverseLogPsiTerm y X 1 l f) = liuPanAggregateInverseLogPrincipalPsiTerm y X 1 f

The actual inverse-log aggregate psi term at modulus one is principal only.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPsiCharacterTerm_eq_principal_add_hyperbola {y X q l : ℕ} (f : ℕ → ℝ) (hq : 0 < q) : liuPanAggregateInverseLogPsiCharacterTerm y X q l f = liuPanAggregateInverseLogPrincipalPsiTerm y X q f + liuPanAggregateNonprincipalLogLambdaHyperbola y X q l f

The complete exact character reduction after Abel substitution: the principal term remains separate, while the nonprincipal part is one coupled source/Lambda hyperbola sum.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPsiCharacterTerm_eq_principal_add_low_add_mediumHigh {y X q l : ℕ} (D₀ : ℕ) (f : ℕ → ℝ) (hq : 0 < q) : liuPanAggregateInverseLogPsiCharacterTerm y X q l f = liuPanAggregateInverseLogPrincipalPsiTerm y X q f + liuPanAggregateLogLambdaLowConductorSum D₀ y X q l f + liuPanAggregateLogLambdaMediumHighConductorSum D₀ y X q l f

The exact three-way analytic split at conductor threshold D₀.

Source-family decomposition

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPrincipalPNTMaxY (N q : ℕ) (f : ℕ → ℝ) : ℝ

Canonical y ≤ N maximum of the ordinary principal PNT-error term.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPrincipalPNTMaxY N q f = (Finset.image (fun (y : ℕ) => ‖MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPrincipalPNTTerm y N q f‖) (Finset.range (N + 1))).max' ⋯

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNonprincipalPsiMaxL (y N q : ℕ) (f : ℕ → ℝ) : ℝ

Canonical reduced-residue maximum of the nonprincipal character term.

Equations

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

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNonprincipalPsiMaxY (N q : ℕ) (f : ℕ → ℝ) : ℝ

Canonical y ≤ N maximum of the nonprincipal character term.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNonprincipalPsiMaxY N q f = (Finset.image (fun (y : ℕ) => MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNonprincipalPsiMaxL y N q f) (Finset.range (N + 1))).max' ⋯

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorMaxL (D₀ y N q : ℕ) (f : ℕ → ℝ) : ℝ

Reduced-residue maximum of the low-conductor primitive hyperbola family.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorMaxL D₀ y N q f = if h : (AnalyticNumberTheory.Sieve.unitResidues q).Nonempty then (Finset.image (fun (l : ℕ) => ‖MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorSum D₀ y N q l f‖) (AnalyticNumberTheory.Sieve.unitResidues q)).max' ⋯ else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaMediumHighConductorMaxL (D₀ y N q : ℕ) (f : ℕ → ℝ) : ℝ

Reduced-residue maximum of the medium/high primitive hyperbola family.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaMediumHighConductorMaxL D₀ y N q f = if h : (AnalyticNumberTheory.Sieve.unitResidues q).Nonempty then (Finset.image (fun (l : ℕ) => ‖MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaMediumHighConductorSum D₀ y N q l f‖) (AnalyticNumberTheory.Sieve.unitResidues q)).max' ⋯ else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorMaxY (D₀ N q : ℕ) (f : ℕ → ℝ) : ℝ

Shared-y maximum of the low-conductor primitive hyperbola family.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorMaxY D₀ N q f = (Finset.image (fun (y : ℕ) => MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorMaxL D₀ y N q f) (Finset.range (N + 1))).max' ⋯

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaMediumHighConductorMaxY (D₀ N q : ℕ) (f : ℕ → ℝ) : ℝ

Shared-y maximum of the medium/high primitive hyperbola family.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaMediumHighConductorMaxY D₀ N q f = (Finset.image (fun (y : ℕ) => MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaMediumHighConductorMaxL D₀ y N q f) (Finset.range (N + 1))).max' ⋯

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

Modulus-weighted ordinary principal PNT-error average.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateInverseLogPrincipalPNTAverage N f B = ∑ q ∈ Finset.range (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B + 1), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight q * MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPrincipalPNTMaxY N q f

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

Modulus-weighted nonprincipal character average, still before any all-character Cauchy--Schwarz estimate.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateInverseLogNonprincipalPsiAverage N f B = ∑ q ∈ Finset.range (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B + 1), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight q * MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNonprincipalPsiMaxY N q f

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateLogLambdaLowConductorAverage (D₀ N : ℕ) (f : ℕ → ℝ) (B : ℝ) : ℝ

Modulus-weighted low-conductor family, retaining the original squarefree-3^omega weights.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateLogLambdaLowConductorAverage D₀ N f B = ∑ q ∈ Finset.range (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B + 1), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight q * MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorMaxY D₀ N q f

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateLogLambdaMediumHighConductorAverage (D₀ N : ℕ) (f : ℕ → ℝ) (B : ℝ) : ℝ

Modulus-weighted medium/high primitive bilinear hyperbola family.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateLogLambdaMediumHighConductorAverage D₀ N f B = ∑ q ∈ Finset.range (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B + 1), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight q * MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaMediumHighConductorMaxY D₀ N q f

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNonprincipalPsiMaxL_le_low_add_mediumHigh (D₀ N y q : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogNonprincipalPsiMaxL y N q f ≤ liuPanAggregateLogLambdaLowConductorMaxL D₀ y N q f + liuPanAggregateLogLambdaMediumHighConductorMaxL D₀ y N q f

The exact conductor partition passes through the reduced-residue maximum using only the final two-term triangle inequality.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNonprincipalPsiMaxY_le_low_add_mediumHigh (D₀ N q : ℕ) (f : ℕ → ℝ) : liuPanAggregateInverseLogNonprincipalPsiMaxY N q f ≤ liuPanAggregateLogLambdaLowConductorMaxY D₀ N q f + liuPanAggregateLogLambdaMediumHighConductorMaxY D₀ N q f

The exact conductor partition passes through the shared-y maximum.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateInverseLogNonprincipalPsiAverage_le_low_add_mediumHigh (D₀ N : ℕ) (f : ℕ → ℝ) (B : ℝ) : liuMainPanAggregateInverseLogNonprincipalPsiAverage N f B ≤ liuMainPanAggregateLogLambdaLowConductorAverage D₀ N f B + liuMainPanAggregateLogLambdaMediumHighConductorAverage D₀ N f B

The modulus-weighted nonprincipal average is bounded by the two exact conductor families, with no all-character Cauchy step.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogNoncoprimeCorrection_nonneg (N y q : ℕ) : 0 ≤ liuPanAggregateInverseLogNoncoprimeCorrection y N q (liuWeight N (liuSourceZ10 N) (liuSourceY3 N))

For Liu's source, the real noncoprime correction is nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanAggregateInverseLogPsiTerm_le_pnt_add_noncoprime_add_nonprincipal {N y q l : ℕ} (hq : 0 < q) (hl : IsUnit ↑l) : |liuPanAggregateInverseLogPsiTerm y N q l (liuWeight N (liuSourceZ10 N) (liuSourceY3 N))| ≤ ‖liuPanAggregateInverseLogPrincipalPNTTerm y N q (liuWeight N (liuSourceZ10 N) (liuSourceY3 N))‖ + liuPanAggregateInverseLogNoncoprimeCorrection y N q (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) / ↑q.totient + ‖liuPanAggregateInverseLogNonprincipalPsiTerm y N q l (liuWeight N (liuSourceZ10 N) (liuSourceY3 N))‖

Pointwise, the aggregate psi term has exactly the ordinary principal PNT error, the positive noncoprime correction, and the nonprincipal character term.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPsiMaxL_le_pnt_add_noncoprime_add_nonprincipal (N y q : ℕ) : liuPanAggregateInverseLogPsiMaxL y N q (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) ≤ ‖liuPanAggregateInverseLogPrincipalPNTTerm y N q (liuWeight N (liuSourceZ10 N) (liuSourceY3 N))‖ + liuPanAggregateInverseLogNoncoprimeCorrection y N q (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) / ↑q.totient + liuPanAggregateInverseLogNonprincipalPsiMaxL y N q (liuWeight N (liuSourceZ10 N) (liuSourceY3 N))

The pointwise split passes through the reduced-residue maximum without mixing the principal and nonprincipal families.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPsiMaxY_le_pnt_add_noncoprime_add_nonprincipal (N q : ℕ) : liuPanAggregateInverseLogPsiMaxY N q N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) ≤ liuPanAggregateInverseLogPrincipalPNTMaxY N q (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) + liuPanAggregateInverseLogNoncoprimeCorrectionMaxY N q / ↑q.totient + liuPanAggregateInverseLogNonprincipalPsiMaxY N q (liuWeight N (liuSourceZ10 N) (liuSourceY3 N))

The three-term split passes through the shared y ≤ N maximum.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateInverseLogPsiAverage_le_decomposition (N : ℕ) (B : ℝ) : liuMainPanAggregateInverseLogPsiAverage N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) B ≤ liuMainPanAggregateInverseLogPrincipalPNTAverage N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) B + liuMainPanAggregateInverseLogNoncoprimeCorrectionAverage N B + liuMainPanAggregateInverseLogNonprincipalPsiAverage N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) B

Exact source-family bookkeeping: the original aggregate psi average is bounded by the ordinary principal PNT family, the now-unconditional noncoprime correction, and the still-conductor-grouped nonprincipal family.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateInverseLogPrincipalPNTMaxY_le_split (D C : ℝ) (hD : 0 < D) (hC : 0 ≤ C) (T0 Ngeom : ℕ) (hscalar : ∀ (t : ℕ), T0 ≤ t → |liuPanLogPNTError t| ≤ C * ↑t / Real.log ↑t ^ D) (hgeom : ∀ (N : ℕ), Ngeom ≤ N → ∀ (y : ℕ), ↑N ^ (5 / 6) ≤ ↑y → ∀ a ∈ Finset.Icc 1 N, liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a ≠ 0 → ↑N ^ (1 / 9) ≤ ↑(y / a)) {N q : ℕ} (hN : 3 ≤ N) (hNgeom : Ngeom ≤ N) (hT0 : ↑T0 ≤ ↑N ^ (1 / 9)) : liuPanAggregateInverseLogPrincipalPNTMaxY N q (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) ≤ (2 * (Real.log 4 + 5) * (Real.log 2)⁻¹ * ↑N ^ (5 / 6) * (1 + Real.log ↑N) + C * 9 ^ D * ↑N / Real.log ↑N ^ D * (1 + Real.log ↑N)) / ↑q.totient

Uniform principal/PNT maximum obtained by splitting y < N^(5/6) from the complementary range.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateInverseLogPrincipalPNTAverage_le_split_mul_H3 (D C : ℝ) (hD : 0 < D) (hC : 0 ≤ C) (T0 Ngeom : ℕ) (hscalar : ∀ (t : ℕ), T0 ≤ t → |liuPanLogPNTError t| ≤ C * ↑t / Real.log ↑t ^ D) (hgeom : ∀ (N : ℕ), Ngeom ≤ N → ∀ (y : ℕ), ↑N ^ (5 / 6) ≤ ↑y → ∀ a ∈ Finset.Icc 1 N, liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a ≠ 0 → ↑N ^ (1 / 9) ≤ ↑(y / a)) {N : ℕ} (B : ℝ) (hN : 3 ≤ N) (hNgeom : Ngeom ≤ N) (hT0 : ↑T0 ≤ ↑N ^ (1 / 9)) : liuMainPanAggregateInverseLogPrincipalPNTAverage N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) B ≤ (2 * (Real.log 4 + 5) * (Real.log 2)⁻¹ * ↑N ^ (5 / 6) * (1 + Real.log ↑N) + C * 9 ^ D * ↑N / Real.log ↑N ^ D * (1 + Real.log ↑N)) * liuPanPrimePowerH3Mass (panModulusCutoff N B)

The split source estimate lifts through exactly the existing H₃ modulus mass, including the totalized zero modulus.

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPrincipalPNTSourceFamilyBound : Prop

Minimal varying-source hypothesis for the ordinary PNT part of the principal character. No pointwise psi(x) ∼ x statement is promoted to this uniform aggregate estimate.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPrincipalPNTSourceFamilyBound = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N0 : ℕ), ∀ (N : ℕ), N0 ≤ N → MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateInverseLogPrincipalPNTAverage N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) B ≤ C * ↑N / Real.log ↑N ^ A

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuMainPanAggregateInverseLogPrincipalPNTAverage_le (A : ℝ) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∃ (N0 : ℕ), ∀ (N : ℕ), N0 ≤ N → ∀ (B : ℝ), 0 ≤ B → liuMainPanAggregateInverseLogPrincipalPNTAverage N (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) B ≤ C * ↑N / Real.log ↑N ^ A

The ordinary principal source family is unconditional. The estimate is uniform in every nonnegative Pan cutoff parameter, which lets it be combined with either nonprincipal conductor regime without changing cutoffs.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateInverseLogPrincipalPNTSourceFamilyBound : LiuMainPanAggregateInverseLogPrincipalPNTSourceFamilyBound

The named principal/PNT source-family contract is therefore inhabited without an additional analytic assumption.

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregatePrincipalPNTBoundAt (A C B : ℝ) (N0 : ℕ) : Prop

A shared-cutoff principal/PNT source-family estimate.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregatePrincipalPNTBoundAt A C B N0 = ∀ (N : ℕ), N0 ≤ N → MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateInverseLogPrincipalPNTAverage N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) B ≤ C * ↑N / Real.log ↑N ^ A

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateLowConductorSiegelWalfiszBoundAt (D₀ : ℕ → ℕ) (A C B : ℝ) (N0 : ℕ) : Prop

The low-conductor Siegel--Walfisz input at a chosen conductor threshold.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateLowConductorSiegelWalfiszBoundAt D₀ A C B N0 = ∀ (N : ℕ), N0 ≤ N → MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateLogLambdaLowConductorAverage (D₀ N) N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) B ≤ C * ↑N / Real.log ↑N ^ A

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateMediumHighConductorBilinearBoundAt (D₀ : ℕ → ℕ) (A C B : ℝ) (N0 : ℕ) : Prop

The medium/high-conductor weighted primitive bilinear hyperbola maximal input at the same conductor threshold and modulus cutoff.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateMediumHighConductorBilinearBoundAt D₀ A C B N0 = ∀ (N : ℕ), N0 ≤ N → MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateLogLambdaMediumHighConductorAverage (D₀ N) N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) B ≤ C * ↑N / Real.log ↑N ^ A

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPsiConductorSplitSourceFamilyBound : Prop

The earlier three-part packaging with one shared modulus cutoff and one conductor threshold function. Its principal component is now unconditional; the predicate is retained as a convenient bundled interface.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPsiConductorSplitSourceFamilyBound = ∀ (A : ℝ), 0 < A → ∃ (D₀ : ℕ → ℕ) (Cpnt : ℝ), 0 < Cpnt ∧ ∃ (Clow : ℝ), 0 < Clow ∧ ∃ (Chigh : ℝ), 0 < Chigh ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N0 : ℕ), MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregatePrincipalPNTBoundAt A Cpnt B N0 ∧ MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateLowConductorSiegelWalfiszBoundAt D₀ A Clow B N0 ∧ MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateMediumHighConductorBilinearBoundAt D₀ A Chigh B N0

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPsiNonprincipalConductorSourceFamilyBound : Prop

The only source-family inputs still open: low primitive conductors and the medium/high primitive bilinear family, at one shared cutoff.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPsiNonprincipalConductorSourceFamilyBound = ∀ (A : ℝ), 0 < A → ∃ (D₀ : ℕ → ℕ) (Clow : ℝ), 0 < Clow ∧ ∃ (Chigh : ℝ), 0 < Chigh ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N0 : ℕ), MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateLowConductorSiegelWalfiszBoundAt D₀ A Clow B N0 ∧ MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateMediumHighConductorBilinearBoundAt D₀ A Chigh B N0

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPsiRemainingSourceFamilyBound : Prop

The two genuinely analytic source-family inputs, stated with one shared modulus cutoff: ordinary PNT for the principal family and the conductor-first nonprincipal estimate. The noncoprime correction is intentionally absent.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPsiRemainingSourceFamilyBound = ∀ (A : ℝ), 0 < A → ∃ (Cpnt : ℝ), 0 < Cpnt ∧ ∃ (Cnonprincipal : ℝ), 0 < Cnonprincipal ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N0 : ℕ), ∀ (N : ℕ), N0 ≤ N → MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateInverseLogPrincipalPNTAverage N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) B ≤ Cpnt * ↑N / Real.log ↑N ^ A ∧ MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateInverseLogNonprincipalPsiAverage N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) B ≤ Cnonprincipal * ↑N / Real.log ↑N ^ A

theorem MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPsiConductorSplitSourceFamilyBound.to_remaining (h : LiuMainPanAggregateInverseLogPsiConductorSplitSourceFamilyBound) : LiuMainPanAggregateInverseLogPsiRemainingSourceFamilyBound

The principal/PNT, low-conductor Siegel--Walfisz, and medium/high weighted primitive bilinear predicates imply the remaining two-family psi predicate.

theorem MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPsiNonprincipalConductorSourceFamilyBound.to_remaining (h : LiuMainPanAggregateInverseLogPsiNonprincipalConductorSourceFamilyBound) : LiuMainPanAggregateInverseLogPsiRemainingSourceFamilyBound

The unconditional principal theorem reduces the remaining two-family predicate to the low and medium/high nonprincipal conductor estimates alone.

theorem MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPsiRemainingSourceFamilyBound.to_psi (h : LiuMainPanAggregateInverseLogPsiRemainingSourceFamilyBound) : LiuMainPanAggregateInverseLogPsiSourceFamilyBound

The remaining PNT/nonprincipal source-family inputs imply the original aggregate psi contract because the noncoprime family is unconditional.

theorem MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPsiConductorSplitSourceFamilyBound.to_psi (h : LiuMainPanAggregateInverseLogPsiConductorSplitSourceFamilyBound) : LiuMainPanAggregateInverseLogPsiSourceFamilyBound

The exact three-regime analytic predicate implies the original aggregate source-family psi contract; the noncoprime correction is supplied unconditionally.

theorem MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateInverseLogPsiNonprincipalConductorSourceFamilyBound.to_psi (h : LiuMainPanAggregateInverseLogPsiNonprincipalConductorSourceFamilyBound) : LiuMainPanAggregateInverseLogPsiSourceFamilyBound

Low-conductor Siegel--Walfisz plus the medium/high primitive bilinear estimate now suffice for the full aggregate psi source-family contract. Principal PNT and noncoprime terms are supplied unconditionally.

Remaining analytic split

The ordinary principal/PNT family is closed unconditionally by liuMainPanAggregateInverseLogPrincipalPNTSourceFamilyBound, and the noncoprime family is also closed unconditionally. Exactly two analytic regimes remain, neither asserted here:

• low primitive conductors, to be treated by Siegel--Walfisz;
• medium and high conductors, requiring a weighted primitive bilinear hyperbola maximal estimate.