theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.vertical_reciprocal_le {σ : ℝ} (hσ : 1 / 2 ≤ σ) (t : ℝ) : 1 / ‖MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t‖ ≤ 3 / (1 + |t|)

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.integral_vertical_log_weight {T : ℝ} (hT : 0 ≤ T) : ∫ (t : ℝ) in -T..T, 1 / (1 + |t|) = 2 * Real.log (1 + T)

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.vertical_reciprocal_integral_le {σ T : ℝ} (hσ : 1 / 2 ≤ σ) (hT : 0 ≤ T) : ∫ (t : ℝ) in -T..T, 1 / ‖MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t‖ ≤ 6 * Real.log (1 + T)

The reciprocal Perron denominator has only logarithmic mass on a vertical segment.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.primitive_integral_mean_le (S : Finset ℕ) (G : (q : ℕ) → PrimitiveCharacter q → ℝ → ℂ) {σ Y T M : ℝ} (hσ : 1 / 2 ≤ σ) (hY : 0 < Y) (hT : 0 ≤ T) (hM : 0 ≤ M) (hG : ∀ q ∈ S, ∀ (χ : PrimitiveCharacter q), Continuous (G q χ)) (hmean : ∀ t ∈ Set.Icc (-T) T, ∑ q ∈ S, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ‖G q χ t‖ ≤ M) : ∑ q ∈ S, (↑q.totient)⁻¹ * ∑ χ : PrimitiveCharacter q, ‖(↑(2 * Real.pi))⁻¹ * ∫ (t : ℝ) in -T..T, G q χ t * ↑Y ^ MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t / MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t‖ ≤ 6 * Y ^ σ * M * Real.log (1 + T)

A uniform primitive-character mean pays just one logarithm under the Perron integral. The complex functions remain intact until taking the norm of their complete integrals.