theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanCoprimeIntervalMaxL_boundedAggregate_log_saving (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (A₁ A₂ : ℕ) (f : ℕ → ℝ), ↑A₂ ≤ ↑N ^ (2 / 3) → Real.log ↑N ^ (2 * B) ≤ ↑A₁ → (∀ (a : ℕ), |f a| ≤ 1) → ∑ d ∈ Finset.Icc 1 (panModulusCutoff N B), liuMainPanCoprimeIntervalMaxL (liuLogarithmicIntegral (2 / Real.log 2)) N A₁ A₂ d f ≤ C * ↑N / Real.log ↑N ^ U

Actual reduced-residue Pan aggregate for any bounded real coefficient. The cutoff exponent is chosen before N, the window, and the coefficient.