theorem AnalyticNumberTheory.LargeSieve.selectorRectangularSmoothedKernelWeightedPrimitiveMean_le (a b : ℤ → ℂ) (Y : (q : ℕ) → PrimitiveCharacter q → ℕ) (Ma Mb : ℤ) (Na Nb Q M : ℕ) (hQ : 0 < Q) (S : Finset ℕ) (hS : S ⊆ Finset.Icc 1 Q) (hM : 3 ≤ M) (hYM : ∀ (q : ℕ) (χ : PrimitiveCharacter q), Y q χ ≤ M) (hm1 : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), 1 ≤ m) (hmM : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), m ≤ ↑M) (hn1 : ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), 1 ≤ n) (hnM : ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), n ≤ ↑M) : ∑ q ∈ S, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖rectangularSmoothedKernelCharacterSum a b (1 / ↑M ^ 2) (MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep (Y q χ)) Ma Mb Na Nb q χ‖ ≤ (1 / 2 + (14 * Real.log ↑M + 4) / Real.pi) * rankOneRectangularLSRHS a b Ma Mb Na Nb Q

Character-wise half-step smoothing still satisfies the same exact damped Perron formula; only the positive-frequency majorant changes. The four selector-separated rank-one lanes contribute respectively 2 log M, log M, log M, and 2 log M, so for ε = M⁻² the integral cost is exactly 14 log M + 4.

theorem AnalyticNumberTheory.LargeSieve.selectorRectangularSharpHyperbolicWeightedPrimitiveMean_le (a b : ℤ → ℂ) (Y : (q : ℕ) → PrimitiveCharacter q → ℕ) (Ma Mb : ℤ) (Na Nb Q M : ℕ) (hQ : 0 < Q) (S : Finset ℕ) (hS : S ⊆ Finset.Icc 1 Q) (hM : 3 ≤ M) (hYM : ∀ (q : ℕ) (χ : PrimitiveCharacter q), Y q χ ≤ M) (hm1 : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), 1 ≤ m) (hmM : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), m ≤ ↑M) (hn1 : ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), 1 ≤ n) (hnM : ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), n ≤ ↑M) (hmnPos : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), 0 < m * n) (hmnM : ∀ m ∈ Finset.Icc (Ma + 1) (Ma + ↑Na), ∀ n ∈ Finset.Icc (Mb + 1) (Mb + ↑Nb), m * n ≤ ↑M) : ∑ q ∈ S, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖rectangularSharpHyperbolicCharacterSum a b (Y q χ) Ma Mb Na Nb q χ‖ ≤ (1 / 2 + (14 * Real.log ↑M + 4) / Real.pi) * rankOneRectangularLSRHS a b Ma Mb Na Nb Q + 8 / (Real.pi * ↑M) * rectangularCoefficientL1 a b Ma Mb Na Nb * weightedPrimitiveFamilyMass S

Character-wise selector version of the sharp hyperbolic rectangular primitive L¹ bound. The smoothed selector mean is paid by the four y-independent phase-separated lanes, and the sharp comparison keeps the exact 8 / (π M) coefficient error.