noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveCofactorLedger (N A₁ A₂ D m : ℕ) (f : ℕ → ℝ) : ℝ

The original whole-source primitive ledger, with the cofactor in both screens.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveCofactorLedger N A₁ A₂ D m f = AnalyticNumberTheory.LargeSieve.PanLow.nonprincipalLow (fun (a : ℕ) => if a.Coprime m then ↑(f a) else 0) (fun (p : ℕ) => if Nat.Prime p ∧ p.Coprime m then 1 else 0) N A₁ A₂ D

theorem MathlibNt.SieveTheory.LiuWeight.liuPanActualNonprincipal_sum_le_cofactor (N A₁ A₂ D : ℕ) (f : ℕ → ℝ) : ∑ q ∈ Finset.Icc 1 D, (↑q.totient)⁻¹ * liuPanActualNonprincipalMass N A₁ A₂ q f ≤ ∑ m ∈ Finset.Icc 1 D, (↑m.totient)⁻¹ * liuPanPrimitiveCofactorLedger N A₁ A₂ D m f

Exact conductor decomposition followed by positive cofactor enlargement. No source-a triangle and no analytic estimate is used.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanActualNonprincipal_sum_le_log_sq (N A₁ A₂ D : ℕ) (f : ℕ → ℝ) (M : ℝ) (hM : 0 ≤ M) (hDN : D ≤ N) (hinner : ∀ m ∈ Finset.Icc 1 D, liuPanPrimitiveCofactorLedger N A₁ A₂ D m f ≤ M) : ∑ q ∈ Finset.Icc 1 D, (↑q.totient)⁻¹ * liuPanActualNonprincipalMass N A₁ A₂ q f ≤ M * (1 + Real.log ↑N) ^ 2

A uniform full primitive estimate pays the original same-modulus mass. The two-log cofactor cost is explicit and is not the printed one-log constant.