theorem AnalyticNumberTheory.LargeSieve.PanLow.nonprincipalLow_eq_low_add_high (g d : ℕ → ℂ) (N A₁ A₂ D₁ D : ℕ) (h1 : 1 ≤ D₁) (hD : D₁ ≤ D) : nonprincipalLow g d N A₁ A₂ D = nonprincipalLow g d N A₁ A₂ D₁ + panIymHigh g d N A₁ A₂ D₁ D

Exact partition after removing the principal conductor-one character.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveCofactorLedger_eq_source (N A₁ A₂ D m : ℕ) (f : ℕ → ℝ) : liuPanPrimitiveCofactorLedger N A₁ A₂ D m f = AnalyticNumberTheory.LargeSieve.PanLow.nonprincipalLow (AnalyticNumberTheory.LargeSieve.panSourceG (fun (a : ℕ) => ↑(f a)) m) (AnalyticNumberTheory.LargeSieve.panSourceD m) N A₁ A₂ D

Both cofactor screens are exactly the canonical high-source screens.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_pan_log_rpow_le_rpow (t r : ℝ) (hr : 0 < r) : ∀ᶠ (N : ℕ) in Filter.atTop, Real.log ↑N ^ t ≤ ↑N ^ r

Elementary eventual payment, used only for powers of log versus powers of N.

theorem MathlibNt.SieveTheory.LiuWeight.panModulusCutoff_eq_upper (N : ℕ) (B : ℝ) : panModulusCutoff N B = ⌊AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.upperConductor N B⌋₊

theorem MathlibNt.SieveTheory.LiuWeight.eventually_pan_conductor_bounds (B : ℝ) (hB : 0 ≤ B) : ∀ᶠ (N : ℕ) in Filter.atTop, 1 ≤ Real.log ↑N ∧ 1 ≤ ⌊AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.lowConductor N B⌋₊ ∧ ⌊AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.lowConductor N B⌋₊ ≤ panModulusCutoff N B ∧ ↑(panModulusCutoff N B) ≤ √↑N ∧ panModulusCutoff N B ≤ N

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveCofactorLedger_log_saving (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ m ∈ Finset.Icc 1 (panModulusCutoff N B), liuPanPrimitiveCofactorLedger N (liuPanSourceIntervalLower N B) (liuPanSourceIntervalUpper N) (panModulusCutoff N B) m (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) ≤ C * ↑N / Real.log ↑N ^ U

Full primitive ledger, uniformly in the cofactor. No high or low estimate is a theorem parameter. The exponent B is chosen before N and m.