Finite-height Perron truncation for the complete Pan source

The existing, proved Perron kernel estimate is used at Pan's actual abscissa and exponential height. Reciprocal product weights are retained in the error: an unweighted count up to the exponential height would lose the saving. Only the truncation remainder is estimated coefficientwise.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.source_pos_of_log {x : ℕ} (hx : 1 ≤ Real.log ↑x) : 0 < x

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.halfStep_ratio_source_power_le {x y n : ℕ} (hx : 1 ≤ Real.log ↑x) (hy : 1 ≤ y) (hyx : y ≤ x) (hn : n ≠ 0) : (MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep y / ↑n) ^ panSourceSigma x ≤ 4 * ↑x ^ 2 / ↑n

The numerator costs a fixed polynomial, while every positive coefficient retains its reciprocal weight.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.source_kernel_error_le {x y n : ℕ} {T : ℝ} (hx : 1 ≤ Real.log ↑x) (hy : 1 ≤ y) (hyx : y ≤ x) (hn : n ≠ 0) (hT : 0 < T) : ‖(if n ≤ y then 1 else 0) - MathlibNt.SieveTheory.LiuWeight.liuPanTruncatedPerronKernel (panSourceSigma x) T (MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep y / ↑n)‖ ≤ 108 * ↑x ^ 3 / T / ↑n

A uniform, weighted kernel error on every positive integer, including coordinates beyond the hyperbola. No kernel approximation is assumed.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.hyperbola_error_le_harmonic {q x y : ℕ} {T : ℝ} (U V : Finset ℕ) (A B : ℕ → ℂ) (χ : DirichletCharacter ℂ q) (hU : ∀ u ∈ U, 0 < u) (hV : ∀ v ∈ V, 0 < v) (hA : ∀ u ∈ U, ‖A u‖ ≤ 1) (hB : ∀ v ∈ V, ‖B v‖ ≤ 1) (hx : 1 ≤ Real.log ↑x) (hy : 1 ≤ y) (hyx : y ≤ x) (hT : 0 < T) : ‖MathlibNt.SieveTheory.LiuWeight.liuPanTruncatedPerronError U V A B χ (panSourceSigma x) T y‖ ≤ (108 * ↑x ^ 3 / T * ∑ u ∈ U, (↑u)⁻¹) * ∑ v ∈ V, (↑v)⁻¹

The full finite hyperbola has a harmonic-mass error, rather than the unusable cardinality of the exponential prime cutoff.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.sourceHeight_ge_pow (K : ℕ) {x : ℕ} (hx : 1 ≤ Real.log ↑x) (hK : ↑K ≤ 2 * Real.log ↑x) : ↑x ^ K ≤ panSourceHeight x

The literal exponential height pays every fixed polynomial loss.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.sourceHeight_floor_ge {x : ℕ} (hx : 1 ≤ Real.log ↑x) : x ≤ ⌊panSourceHeight x⌋₊

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.source_hyperbola_error_le {q x y : ℕ} (U V : Finset ℕ) (A B : ℕ → ℂ) (χ : DirichletCharacter ℂ q) (hU : U ⊆ Finset.Icc 1 x) (hV : V ⊆ Finset.Icc 1 ⌊panSourceHeight x⌋₊) (hA : ∀ u ∈ U, ‖A u‖ ≤ 1) (hB : ∀ v ∈ V, ‖B v‖ ≤ 1) (hx : 4 ≤ Real.log ↑x) (hy : 1 ≤ y) (hyx : y ≤ x) : ‖MathlibNt.SieveTheory.LiuWeight.liuPanTruncatedPerronError U V A B χ (panSourceSigma x) (panSourceHeight x) y‖ ≤ 324 * (↑x ^ 2)⁻¹

Uniform error at the actual height, even though the second polynomial contains every coordinate through floor T.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.source_amplitude_eq_hyperbola {q : ℕ} (A B : ℕ → ℂ) (y L U M : ℕ) (χ : PrimitiveCharacter q) (hyM : y ≤ M) : panSourceCharacterAmplitude A B y L U χ = MathlibNt.SieveTheory.LiuWeight.liuPanPerronHyperbolaSum (Finset.Ioc L U) (Finset.Icc 1 M) A B (↑χ) y

Exact integer hyperbola, including equality at a*n=y. The common half-step is applied to the product, not separately to each source row.

theorem AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.source_amplitude_perron {q x y : ℕ} (f : ℕ → ℂ) (hf : ∀ (n : ℕ), ‖f n‖ ≤ 1) (m L U : ℕ) (χ : PrimitiveCharacter q) (hx : 4 ≤ Real.log ↑x) (hy : 1 ≤ y) (hyx : y ≤ x) (hUx : U ≤ x) : ‖panSourceCharacterAmplitude (panSourceG f m) (panSourceD m) y L U χ - MathlibNt.SieveTheory.LiuWeight.liuPanTruncatedPerronIntegral (Finset.Ioc L U) (Finset.Icc 1 ⌊panSourceHeight x⌋₊) (panSourceG f m) (panSourceD m) (↑χ) (panSourceSigma x) (panSourceHeight x) y‖ ≤ 324 * (↑x ^ 2)⁻¹

Perron's formula for the complete source/prime amplitude, at Pan's line and height, with an unconditional error uniform in the source and character.