Pan (2.4), first line only: actual prime counts, with the true principal remainder retained. No analytic estimate or conductor decomposition is used.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanActualCharacterAmplitude (N A₁ A₂ q : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : ℂ

Same-modulus complete amplitude; the whole source sum is inside the norm.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanActualCharacterAmplitude N A₁ A₂ q f χ = ∑ a ∈ Finset.Ioc A₁ A₂, if a.Coprime q then ↑(f a) * χ ↑a * ∑ p ∈ Finset.range (N / a + 1), if Nat.Prime p ∧ p.Coprime q then χ ↑p else 0 else 0

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

Raw principal remainder: not divided by phi, and not a free predicate.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanActualPrincipalRaw main N A₁ A₂ q f = ∑ a ∈ Finset.Ioc A₁ A₂, if a.Coprime q then f a * ((∑ p ∈ Finset.range (N / a + 1), if Nat.Prime p ∧ p.Coprime q then 1 else 0) - main (↑N / ↑a)) else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanActualNonprincipalMass (N A₁ A₂ q : ℕ) (f : ℕ → ℝ) : ℝ

Every nonprincipal character of the SAME modulus, with no a-triangle.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanActualNonprincipalMass N A₁ A₂ q f = ∑ χ ∈ Finset.univ.erase 1, ‖MathlibNt.SieveTheory.LiuWeight.liuPanActualCharacterAmplitude N A₁ A₂ q f χ‖

theorem MathlibNt.SieveTheory.LiuWeight.liuPanActualCount_eq_characterMean (N A₁ A₂ q l : ℕ) (f : ℕ → ℝ) (hq : 0 < q) (hl : IsUnit ↑l) : (∑ a ∈ Finset.Ioc A₁ A₂, if a.Coprime q then ↑(f a) * ↑(AnalyticNumberTheory.Sieve.primesInAPBelow N a q l) else 0) = (↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q, star (χ ↑l) * liuPanActualCharacterAmplitude N A₁ A₂ q f χ

theorem MathlibNt.SieveTheory.LiuWeight.liuPanActualCharacterAmplitude_one (N A₁ A₂ q : ℕ) (f : ℕ → ℝ) : liuPanActualCharacterAmplitude N A₁ A₂ q f 1 = ∑ a ∈ Finset.Ioc A₁ A₂, if a.Coprime q then ↑(f a) * ∑ p ∈ Finset.range (N / a + 1), if Nat.Prime p ∧ p.Coprime q then 1 else 0 else 0

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeIntervalSum_eq_actualCharacterExpansion (main : ℝ → ℝ) (N A₁ A₂ q l : ℕ) (f : ℕ → ℝ) (hq : 0 < q) (hl : IsUnit ↑l) : ↑(liuMainPanCoprimeIntervalSum main N A₁ A₂ q l f) = (∑ χ ∈ Finset.univ.erase 1, star (χ ↑l) * liuPanActualCharacterAmplitude N A₁ A₂ q f χ + ↑(liuPanActualPrincipalRaw main N A₁ A₂ q f)) / ↑q.totient

Exact complex error decomposition. The phase star(chi(l)) and chi(a) remain coupled until AFTER the complete source summation.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuMainPanCoprimeIntervalSum_le_actualCharacterMass (main : ℝ → ℝ) (N A₁ A₂ q l : ℕ) (f : ℕ → ℝ) (hq : 0 < q) (hl : IsUnit ↑l) : |liuMainPanCoprimeIntervalSum main N A₁ A₂ q l f| ≤ (liuPanActualNonprincipalMass N A₁ A₂ q f + |liuPanActualPrincipalRaw main N A₁ A₂ q f|) / ↑q.totient

Only the outer residue phase is removed; each full a-amplitude survives.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeIntervalMaxL_le_actualCharacterMass (main : ℝ → ℝ) (N A₁ A₂ q : ℕ) (f : ℕ → ℝ) (hq : 0 < q) : liuMainPanCoprimeIntervalMaxL main N A₁ A₂ q f ≤ (liuPanActualNonprincipalMass N A₁ A₂ q f + |liuPanActualPrincipalRaw main N A₁ A₂ q f|) / ↑q.totient

Standard reduced-residue maximum, including q=1 and its residue zero.

theorem MathlibNt.SieveTheory.LiuWeight.liuWeight_intervalMaxL_le_nonprincipal_add_principal (κ : ℝ) (N z10 y3 A₁ A₂ q : ℕ) (hq : 1 ≤ q) : liuMainPanCoprimeIntervalMaxL (liuLogarithmicIntegral κ) N A₁ A₂ q (liuWeight N z10 y3) ≤ (liuPanActualNonprincipalMass N A₁ A₂ q (liuWeight N z10 y3) + |liuPanActualPrincipalRaw (liuLogarithmicIntegral κ) N A₁ A₂ q (liuWeight N z10 y3)|) / ↑q.totient

The required actual Liu specialization, with real N/a in Li and raw P.

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeIntervalMaxL_modulus_zero (main : ℝ → ℝ) (N A₁ A₂ : ℕ) (f : ℕ → ℝ) : liuMainPanCoprimeIntervalMaxL main N A₁ A₂ 0 f = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuPanActualCharacterAmplitude_eq_panSource (N A₁ A₂ q : ℕ) (f : ℕ → ℝ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) : liuPanActualCharacterAmplitude N A₁ A₂ q f ↑χ = AnalyticNumberTheory.LargeSieve.panSourceCharacterAmplitude (fun (a : ℕ) => if a.Coprime q then ↑(f a) else 0) (fun (p : ℕ) => if Nat.Prime p ∧ p.Coprime q then 1 else 0) N A₁ A₂ χ

On primitive inputs this is exactly the existing literal Pan amplitude, with m=q in both coprimality screens. This is an identity, not a conductor step.

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanActualNonprincipalMass_one (N A₁ A₂ : ℕ) (f : ℕ → ℝ) : liuPanActualNonprincipalMass N A₁ A₂ 1 f = 0

Modulus one has no nonprincipal mass; its canonical residue is zero.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeIntervalMaxL_one_eq_principal (main : ℝ → ℝ) (N A₁ A₂ : ℕ) (f : ℕ → ℝ) : liuMainPanCoprimeIntervalMaxL main N A₁ A₂ 1 f = |liuPanActualPrincipalRaw main N A₁ A₂ 1 f|