A finite Perron consumer for Liu's primitive hyperbola

This module supplies only the exact finite algebra needed by a later Perron argument. The truncated-kernel approximation is an explicit hypothesis; no analytic estimate for that kernel is asserted here.

def MathlibNt.SieveTheory.LiuWeight.liuPanPerronZeroExtension (A : ℕ → ℂ) (n : ℕ) : ℂ

A coefficient sequence extended by zero at the forbidden coordinate 0.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPerronZeroExtension A n = if n = 0 then 0 else A n

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPerronZeroExtension_zero (A : ℕ → ℂ) : liuPanPerronZeroExtension A 0 = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPerronZeroExtension_of_ne (A : ℕ → ℂ) {n : ℕ} (hn : n ≠ 0) : liuPanPerronZeroExtension A n = A n

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPerronNatPower (n : ℕ) (s : ℂ) : ℂ

The positive-real power used in the finite Dirichlet polynomials.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPerronNatPower n s = if n = 0 then 0 else Complex.exp (-s * ↑(Real.log ↑n))

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPerronNatPower_zero (s : ℂ) : liuPanPerronNatPower 0 s = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPerronNatPower_of_ne {n : ℕ} (hn : n ≠ 0) (s : ℂ) : liuPanPerronNatPower n s = Complex.exp (-s * ↑(Real.log ↑n))

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPerronDirichletPolynomial {q : ℕ} (U : Finset ℕ) (A : ℕ → ℂ) (χ : DirichletCharacter ℂ q) (s : ℂ) : ℂ

A finite Dirichlet polynomial twisted by a character. The zero coordinate, if present in the supplied finset, contributes exactly zero.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPerronDirichletPolynomial U A χ s = ∑ u ∈ U, MathlibNt.SieveTheory.LiuWeight.liuPanPerronZeroExtension A u * χ ↑u * MathlibNt.SieveTheory.LiuWeight.liuPanPerronNatPower u s

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPerronProductCoefficient {q : ℕ} (A B : ℕ → ℂ) (χ : DirichletCharacter ℂ q) (u v : ℕ) : ℂ

The coefficient of a positive product coordinate. It is zero if either coordinate is zero.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPerronProductCoefficient A B χ u v = if u = 0 ∨ v = 0 then 0 else A u * B v * χ ↑(u * v)

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPerronDirichletPolynomial_mul {q : ℕ} (U V : Finset ℕ) (A B : ℕ → ℂ) (χ : DirichletCharacter ℂ q) (s : ℂ) : liuPanPerronDirichletPolynomial U A χ s * liuPanPerronDirichletPolynomial V B χ s = ∑ u ∈ U, ∑ v ∈ V, liuPanPerronProductCoefficient A B χ u v * liuPanPerronNatPower (u * v) s

Exact finite factorization of the two twisted Dirichlet polynomials.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPerronHyperbolaSum {q : ℕ} (U V : Finset ℕ) (A B : ℕ → ℂ) (χ : DirichletCharacter ℂ q) (Y : ℕ) : ℂ

The exact finite character-twisted hyperbola sum.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPerronHyperbolaSum U V A B χ Y = ∑ u ∈ U, ∑ v ∈ V, if u * v ≤ Y then MathlibNt.SieveTheory.LiuWeight.liuPanPerronProductCoefficient A B χ u v else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep (Y : ℕ) : ℝ

The half-integer Perron cutoff.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep Y = ↑Y + 1 / 2

theorem MathlibNt.SieveTheory.LiuWeight.natCast_lt_liuPanPerronHalfStep_iff {n Y : ℕ} : ↑n < liuPanPerronHalfStep Y ↔ n ≤ Y

theorem MathlibNt.SieveTheory.LiuWeight.natCast_ne_liuPanPerronHalfStep (n Y : ℕ) : ↑n ≠ liuPanPerronHalfStep Y

theorem MathlibNt.SieveTheory.LiuWeight.one_half_le_abs_liuPanPerronHalfStep_sub_natCast (n Y : ℕ) : 1 / 2 ≤ |liuPanPerronHalfStep Y - ↑n|

Every integer stays at least one half away from the half-step cutoff.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep_div_natCast_pos {n Y : ℕ} (hn : n ≠ 0) : 0 < liuPanPerronHalfStep Y / ↑n

The ratio occurring in the Perron kernel is positive at every positive integer coordinate.

theorem MathlibNt.SieveTheory.LiuWeight.one_div_four_mul_le_abs_log_liuPanPerronHalfStep_div {n Y M : ℕ} (hn : n ≠ 0) (hM : 1 ≤ M) (hYM : Y ≤ M) (hnM : n ≤ M) : 1 / (4 * ↑M) ≤ |Real.log (liuPanPerronHalfStep Y / ↑n)|

Uniform separation from the logarithmic singularity on a box of side M. The constant 1 / (4 * M) is deliberately safe at the upper half-step M + 1 / 2.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPerronSigma (M : ℕ) : ℝ

The standard Perron line offset 1 / log M.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPerronSigma M = (Real.log ↑M)⁻¹

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPerronHeight (M : ℕ) : ℝ

The standard quadratic truncation height.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPerronHeight M = ↑M ^ 2

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPerronSigma_pos {M : ℕ} (hM : 3 ≤ M) : 0 < liuPanPerronSigma M

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPerronHeight_pos {M : ℕ} (hM : 1 ≤ M) : 0 < liuPanPerronHeight M

theorem MathlibNt.SieveTheory.LiuWeight.rpow_liuPanPerronSigma_le_exp_one {x : ℝ} {M : ℕ} (hM : 3 ≤ M) (hx : 0 < x) (hxM : x ≤ ↑M) : x ^ liuPanPerronSigma M ≤ Real.exp 1

On the standard Perron line, x^sigma costs at most e throughout the box 0 < x ≤ M.

theorem MathlibNt.SieveTheory.LiuWeight.natCast_rpow_neg_liuPanPerronSigma_le_one {n M : ℕ} (hn : 1 ≤ n) (hM : 3 ≤ M) : ↑n ^ (-liuPanPerronSigma M) ≤ 1

Positive integer coordinates contribute no growth from n^(-sigma).

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine (σ t : ℝ) : ℂ

The vertical line sigma + it.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t = ↑σ + ↑t * Complex.I

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanTruncatedPerronKernel (σ T z : ℝ) : ℂ

The classical truncated Perron kernel after parametrizing the vertical segment by its imaginary coordinate.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanTruncatedPerronKernel σ T z = (↑(2 * Real.pi))⁻¹ * ∫ (t : ℝ) in -T..T, Complex.exp (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t * ↑(Real.log z)) / MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t

def MathlibNt.SieveTheory.LiuWeight.LiuPanTruncatedPerronKernelApproximationAt (σ T ε : ℝ) (Y : ℕ) : Prop

A uniform truncated-kernel approximation at the half-integer cutoff. This is an analytic input, not an assertion made by this module.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuPanTruncatedPerronKernelApproximationAt σ T ε Y = (0 < σ ∧ 0 ≤ ε ∧ ∀ (n : ℕ), n ≠ 0 → ‖(if n ≤ Y then 1 else 0) - MathlibNt.SieveTheory.LiuWeight.liuPanTruncatedPerronKernel σ T (MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep Y / ↑n)‖ ≤ ε)

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanTruncatedPerronIntegral {q : ℕ} (U V : Finset ℕ) (A B : ℕ → ℂ) (χ : DirichletCharacter ℂ q) (σ T : ℝ) (Y : ℕ) : ℂ

The actual vertical-line integral of the product of the two finite Dirichlet polynomials.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanTruncatedPerronIntegral U V A B χ σ T Y = (↑(2 * Real.pi))⁻¹ * ∫ (t : ℝ) in -T..T, Complex.exp (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t * ↑(Real.log (MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep Y))) / MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t * (MathlibNt.SieveTheory.LiuWeight.liuPanPerronDirichletPolynomial U A χ (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t) * MathlibNt.SieveTheory.LiuWeight.liuPanPerronDirichletPolynomial V B χ (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t))

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanTruncatedPerronError {q : ℕ} (U V : Finset ℕ) (A B : ℕ → ℂ) (χ : DirichletCharacter ℂ q) (σ T : ℝ) (Y : ℕ) : ℂ

The exact remainder after replacing the hyperbola cutoff by the truncated Perron integral.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanTruncatedPerronError U V A B χ σ T Y = MathlibNt.SieveTheory.LiuWeight.liuPanPerronHyperbolaSum U V A B χ Y - MathlibNt.SieveTheory.LiuWeight.liuPanTruncatedPerronIntegral U V A B χ σ T Y

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPerronCoefficientMass (U : Finset ℕ) (A : ℕ → ℂ) : ℝ

The l1 mass of a finite coefficient family, with the zero coordinate discarded exactly.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPerronCoefficientMass U A = ∑ u ∈ U, ‖MathlibNt.SieveTheory.LiuWeight.liuPanPerronZeroExtension A u‖

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPerronKernelIntegrand_add_neg {σ : ℝ} (hσ : 0 < σ) (z t : ℝ) : Complex.exp (liuPanPerronLine σ t * ↑(Real.log z)) / liuPanPerronLine σ t + Complex.exp (liuPanPerronLine σ (-t) * ↑(Real.log z)) / liuPanPerronLine σ (-t) = ↑(2 * Real.exp (σ * Real.log z) * (σ * Real.cos (t * Real.log z) + t * Real.sin (t * Real.log z)) / (σ ^ 2 + t ^ 2))

Pairing heights t and -t turns the complex Perron integrand into an explicit real-valued cosine/sine expression.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanTruncatedPerronKernel_eq_paired_real_integral {σ : ℝ} (hσ : 0 < σ) (T z : ℝ) : liuPanTruncatedPerronKernel σ T z = (↑(2 * Real.pi))⁻¹ * ∫ (t : ℝ) in 0..T, ↑(2 * Real.exp (σ * Real.log z) * (σ * Real.cos (t * Real.log z) + t * Real.sin (t * Real.log z)) / (σ ^ 2 + t ^ 2))

Exact real cosine/sine form of the truncated Perron kernel. This is only an algebraic pairing identity; it does not assert a kernel approximation.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanPerronSineTailBound (a T S : ℝ) : a ≠ 0 → 0 < T → T ≤ S → |∫ (t : ℝ) in T..S, Real.sin (a * t) / t| ≤ 3 / (|a| * T)

The finite oscillatory sine tail needed for the quantitative Perron approximation. Integration by parts gives the explicit constant 3.

theorem MathlibNt.SieveTheory.LiuWeight.cauchySeq_liuPanPerronSincIntegral : CauchySeq fun (A : ℝ) => ∫ (x : ℝ) in 0..A, Real.sinc x

The finite sinc integrals form a Cauchy sequence at infinity. This is the convergence part of Dirichlet's integral, independent of its normalization.

theorem MathlibNt.SieveTheory.LiuWeight.exists_liuPanPerronSincIntegralLimit : ∃ (L : ℝ), Filter.Tendsto (fun (A : ℝ) => ∫ (x : ℝ) in 0..A, Real.sinc x) Filter.atTop (nhds L)

The one-sided sinc integral has a finite limit.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanIntegralIoiExpNegMulSinc_eq_arctan_inv (a : ℝ) (ha : 0 < a) : ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-a * x) * Real.sinc x = Real.arctan a⁻¹

def MathlibNt.SieveTheory.LiuWeight.LiuPanPerronSincNormalization : Prop

The single normalization input still needed to identify the convergent Dirichlet integral. Later Perron estimates depend on this proposition rather than silently assuming the value of the limit.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuPanPerronSincNormalization = Filter.Tendsto (fun (A : ℝ) => ∫ (x : ℝ) in 0..A, Real.sinc x) Filter.atTop (nhds (Real.pi / 2))

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPerronSincNormalization : LiuPanPerronSincNormalization

Dirichlet's one-sided sinc integral has the classical value π / 2.

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_liuPanPerronSineIntegral_atTop {a : ℝ} (ha : a ≠ 0) : Filter.Tendsto (fun (T : ℝ) => ∫ (t : ℝ) in 0..T, Real.sin (a * t) / t) Filter.atTop (nhds (if 0 < a then Real.pi / 2 else -(Real.pi / 2)))

The unregularized sine integral has its signed Dirichlet limit at every nonzero frequency.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanPerronSineIntegral_sub_limit_le {a T : ℝ} (ha : a ≠ 0) (hT : 0 < T) : |(∫ (t : ℝ) in 0..T, Real.sin (a * t) / t) - if 0 < a then Real.pi / 2 else -(Real.pi / 2)| ≤ 3 / (|a| * T)

The signed sine integral differs from its Dirichlet limit by the same explicit constant-three tail used in the Perron truncation.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanPerronPoissonCosineTail_le {σ a T S : ℝ} (hσ : 0 < σ) (hT : 0 < T) (hTS : T ≤ S) : |∫ (t : ℝ) in T..S, σ * Real.cos (a * t) / (σ ^ 2 + t ^ 2)| ≤ σ / T

The absolutely convergent cosine part of the paired Perron kernel has an explicit finite tail.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanPerronPoissonSineTail_le {σ a T S : ℝ} (hσ : 0 < σ) (ha : a ≠ 0) (hT : 0 < T) (hTS : T ≤ S) : |∫ (t : ℝ) in T..S, t * Real.sin (a * t) / (σ ^ 2 + t ^ 2)| ≤ 3 / (|a| * T) + σ / (2 * T)

After removing the Dirichlet sine kernel, the remaining t-sine part is absolutely bounded by σ / (2T). Together with the sine-tail estimate this gives the quantitative conditional tail needed for the Poisson component.

theorem MathlibNt.SieveTheory.LiuWeight.exists_liuPanPerronPoissonCosineIntegralLimit {σ a : ℝ} (hσ : 0 < σ) : ∃ (L : ℝ), Filter.Tendsto (fun (T : ℝ) => ∫ (t : ℝ) in 0..T, σ * Real.cos (a * t) / (σ ^ 2 + t ^ 2)) Filter.atTop (nhds L)

The finite cosine integrals have an improper limit. Its explicit Poisson value is a separate normalization step.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanPerronPoissonCosineIntegral_sub_limit_le {σ a L T : ℝ} (hσ : 0 < σ) (hT : 0 < T) (hlim : Filter.Tendsto (fun (S : ℝ) => ∫ (t : ℝ) in 0..S, σ * Real.cos (a * t) / (σ ^ 2 + t ^ 2)) Filter.atTop (nhds L)) : |(∫ (t : ℝ) in 0..T, σ * Real.cos (a * t) / (σ ^ 2 + t ^ 2)) - L| ≤ σ / T

Any limit of the cosine component inherits the explicit σ / T error.

theorem MathlibNt.SieveTheory.LiuWeight.exists_liuPanPerronPoissonSineIntegralLimit {σ a : ℝ} (hσ : 0 < σ) (ha : a ≠ 0) : ∃ (L : ℝ), Filter.Tendsto (fun (T : ℝ) => ∫ (t : ℝ) in 0..T, t * Real.sin (a * t) / (σ ^ 2 + t ^ 2)) Filter.atTop (nhds L)

The finite t-sine integrals have an improper limit for every nonzero frequency. The remaining Poisson identity is the exact evaluation of this limit.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuPanPerronPoissonSineIntegral_sub_limit_le {σ a L T : ℝ} (hσ : 0 < σ) (ha : a ≠ 0) (hT : 0 < T) (hlim : Filter.Tendsto (fun (S : ℝ) => ∫ (t : ℝ) in 0..S, t * Real.sin (a * t) / (σ ^ 2 + t ^ 2)) Filter.atTop (nhds L)) : |(∫ (t : ℝ) in 0..T, t * Real.sin (a * t) / (σ ^ 2 + t ^ 2)) - L| ≤ 3 / (|a| * T) + σ / (2 * T)

Any limit of the t-sine component inherits the sine-tail error plus the absolutely convergent Poisson correction.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPerronPoissonContourIntegrand (σ a : ℝ) (s : ℂ) : ℂ

The complex integrand whose real part is the sum of the two Poisson components in the paired Perron kernel.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPerronPoissonContourIntegrand σ a s = Complex.exp (↑a * Complex.I * s) / (↑σ + Complex.I * s)

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPerronPoissonUpperRectangle_residue {σ a R : ℝ} (hσ : 0 < σ) (hσR : σ < R) : RectangleIntegral' (liuPanPerronPoissonContourIntegrand σ a) (-↑R) (↑R + ↑R * Complex.I) = Complex.exp (-(↑a * ↑σ)) / Complex.I

The upper rectangle encloses the sole pole of the combined Poisson integrand, with its residue evaluated exactly.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPerronPoissonContourIntegrand_add_neg {σ : ℝ} (hσ : 0 < σ) (a t : ℝ) : liuPanPerronPoissonContourIntegrand σ a ↑t + liuPanPerronPoissonContourIntegrand σ a (-↑t) = ↑(2 * (σ * Real.cos (a * t) + t * Real.sin (a * t)) / (σ ^ 2 + t ^ 2))

Pairing the contour integrand on the real axis recovers exactly the sum of the cosine and t-sine Poisson components.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPerronPoissonUpperRectangle_boundary {σ a R : ℝ} (hσ : 0 < σ) (hσR : σ < R) : RectangleIntegral (liuPanPerronPoissonContourIntegrand σ a) (-↑R) (↑R + ↑R * Complex.I) = ↑(2 * Real.pi * Real.exp (-(a * σ)))

Unnormalizing the residue theorem gives the exact boundary integral required before estimating the three non-real sides of the square.

theorem MathlibNt.SieveTheory.LiuWeight.norm_liuPanPerronPoissonHorizontalIntegral_le {σ a R : ℝ} (hσ : 0 ≤ σ) (hR : 2 * σ < R) : ‖HIntegral (liuPanPerronPoissonContourIntegrand σ a) (-R) R R‖ ≤ 4 * Real.exp (-a * R)

The top edge of the Poisson rectangle has an explicit exponentially decaying bound once its height is more than twice the pole height.

theorem MathlibNt.SieveTheory.LiuWeight.norm_liuPanPerronPoissonVerticalRightIntegral_le {σ a R : ℝ} (ha : 0 < a) (hR : 0 < R) : ‖VIntegral (liuPanPerronPoissonContourIntegrand σ a) R 0 R‖ ≤ 1 / (a * R)

The right vertical edge of the Poisson rectangle is bounded by 1 / (aR).

theorem MathlibNt.SieveTheory.LiuWeight.norm_liuPanPerronPoissonVerticalLeftIntegral_le {σ a R : ℝ} (ha : 0 < a) (hR : 0 < R) : ‖VIntegral (liuPanPerronPoissonContourIntegrand σ a) (-R) 0 R‖ ≤ 1 / (a * R)

The left vertical edge of the Poisson rectangle is bounded by 1 / (aR).

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_liuPanPerronPoissonHorizontalIntegral_atTop {σ a : ℝ} (hσ : 0 ≤ σ) (ha : 0 < a) : Filter.Tendsto (fun (R : ℝ) => HIntegral (liuPanPerronPoissonContourIntegrand σ a) (-R) R R) Filter.atTop (nhds 0)

The top edge of the upper Poisson rectangle vanishes as its height tends to infinity.

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_liuPanPerronPoissonVerticalRightIntegral_atTop {σ a : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (R : ℝ) => VIntegral (liuPanPerronPoissonContourIntegrand σ a) R 0 R) Filter.atTop (nhds 0)

The right vertical edge of the upper Poisson rectangle vanishes as its width tends to infinity.

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_liuPanPerronPoissonVerticalLeftIntegral_atTop {σ a : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (R : ℝ) => VIntegral (liuPanPerronPoissonContourIntegrand σ a) (-R) 0 R) Filter.atTop (nhds 0)

The left vertical edge of the upper Poisson rectangle vanishes as its width tends to infinity.

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_liuPanPerronPoissonRealIntegral_atTop {σ a : ℝ} (hσ : 0 < σ) (ha : 0 < a) : Filter.Tendsto (fun (R : ℝ) => HIntegral (liuPanPerronPoissonContourIntegrand σ a) (-R) R 0) Filter.atTop (nhds ↑(2 * Real.pi * Real.exp (-(a * σ))))

Sending the three non-real edges of the upper rectangle to infinity identifies the whole real-axis contour integral.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPerronPoissonRealIntegral_eq_paired {σ : ℝ} (hσ : 0 < σ) (a R : ℝ) : HIntegral (liuPanPerronPoissonContourIntegrand σ a) (-R) R 0 = ∫ (t : ℝ) in 0..R, ↑(2 * (σ * Real.cos (a * t) + t * Real.sin (a * t)) / (σ ^ 2 + t ^ 2))

Pairing the negative and positive halves of the real edge gives the finite cosine-plus-sine Poisson integral exactly.

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_liuPanPerronPoissonCosineIntegral_atTop {σ a : ℝ} (hσ : 0 < σ) : Filter.Tendsto (fun (T : ℝ) => ∫ (t : ℝ) in 0..T, σ * Real.cos (a * t) / (σ ^ 2 + t ^ 2)) Filter.atTop (nhds (Real.pi / 2 * Real.exp (-(|a| * σ))))

The cosine component of the Poisson kernel has its exact improper value for every real frequency.

theorem MathlibNt.SieveTheory.LiuWeight.tendsto_liuPanPerronPoissonSineIntegral_atTop {σ a : ℝ} (hσ : 0 < σ) (ha : a ≠ 0) : Filter.Tendsto (fun (T : ℝ) => ∫ (t : ℝ) in 0..T, t * Real.sin (a * t) / (σ ^ 2 + t ^ 2)) Filter.atTop (nhds ((if 0 < a then Real.pi / 2 else -(Real.pi / 2)) * Real.exp (-(|a| * σ))))

The t-sine component of the Poisson kernel has the signed exact improper value at every nonzero frequency.

theorem MathlibNt.SieveTheory.LiuWeight.norm_liuPanTruncatedPerronKernel_sub_indicator_le {σ T z : ℝ} (hσ : 0 < σ) (hT : 0 < T) (hz : 0 < z) (hz1 : z ≠ 1) : ‖(if 1 < z then 1 else 0) - liuPanTruncatedPerronKernel σ T z‖ ≤ z ^ σ / Real.pi * (3 / (|Real.log z| * T) + 3 * σ / (2 * T))

Explicit truncation error for the Perron kernel away from its jump.

theorem MathlibNt.SieveTheory.LiuWeight.one_div_eight_mul_le_abs_log_liuPanPerronHalfStep_div {n Y M : ℕ} (hn : n ≠ 0) (hM : 1 ≤ M) (hYM : Y ≤ M) : 1 / (8 * ↑M) ≤ |Real.log (liuPanPerronHalfStep Y / ↑n)|

The half-step logarithm stays uniformly separated from zero for every positive integer coordinate, not only those inside the box.

theorem MathlibNt.SieveTheory.LiuWeight.norm_liuPanTruncatedPerronKernel_standard_halfStep_le {n Y M : ℕ} (hn : n ≠ 0) (hM : 3 ≤ M) (hYM : Y ≤ M) : ‖(if n ≤ Y then 1 else 0) - liuPanTruncatedPerronKernel (liuPanPerronSigma M) (liuPanPerronHeight M) (liuPanPerronHalfStep Y / ↑n)‖ ≤ 32 * Real.exp 2 / ↑M

At the standard line and quadratic height, the half-step Perron kernel has a uniform O(1/M) error over every positive integer coordinate.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanTruncatedPerronKernelApproximationAt_standard {Y M : ℕ} (hM : 3 ≤ M) (hYM : Y ≤ M) : LiuPanTruncatedPerronKernelApproximationAt (liuPanPerronSigma M) (liuPanPerronHeight M) (32 * Real.exp 2 / ↑M) Y

The standard Perron parameters satisfy the finite consumer's approximation hypothesis unconditionally.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanTruncatedPerronIntegral_eq_kernelSum {q : ℕ} (U V : Finset ℕ) (A B : ℕ → ℂ) (χ : DirichletCharacter ℂ q) {σ T : ℝ} (Y : ℕ) (hσ : 0 < σ) : liuPanTruncatedPerronIntegral U V A B χ σ T Y = ∑ u ∈ U, ∑ v ∈ V, liuPanPerronProductCoefficient A B χ u v * liuPanTruncatedPerronKernel σ T (liuPanPerronHalfStep Y / ↑(u * v))

Expanding the finite Dirichlet polynomials and interchanging their finite sums with the interval integral gives the exact kernel sum.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPerronHyperbolaSum_eq_integral_add_error {q : ℕ} (U V : Finset ℕ) (A B : ℕ → ℂ) (χ : DirichletCharacter ℂ q) (σ T : ℝ) (Y : ℕ) : liuPanPerronHyperbolaSum U V A B χ Y = liuPanTruncatedPerronIntegral U V A B χ σ T Y + liuPanTruncatedPerronError U V A B χ σ T Y

The exact Perron decomposition, with the approximation error still visible as a single complex remainder.

theorem MathlibNt.SieveTheory.LiuWeight.norm_liuPanTruncatedPerronError_le {q : ℕ} (U V : Finset ℕ) (A B : ℕ → ℂ) (χ : DirichletCharacter ℂ q) {σ T ε : ℝ} (Y : ℕ) (happrox : LiuPanTruncatedPerronKernelApproximationAt σ T ε Y) : ‖liuPanTruncatedPerronError U V A B χ σ T Y‖ ≤ ε * liuPanPerronCoefficientMass U A * liuPanPerronCoefficientMass V B

Any uniform half-step approximation for the truncated kernel gives the expected product-of-l1-masses error bound.

theorem MathlibNt.SieveTheory.LiuWeight.norm_liuPanTruncatedPerronError_standard_le {q : ℕ} (U V : Finset ℕ) (A B : ℕ → ℂ) (χ : DirichletCharacter ℂ q) {Y M : ℕ} (hM : 3 ≤ M) (hYM : Y ≤ M) : ‖liuPanTruncatedPerronError U V A B χ (liuPanPerronSigma M) (liuPanPerronHeight M) Y‖ ≤ 32 * Real.exp 2 / ↑M * liuPanPerronCoefficientMass U A * liuPanPerronCoefficientMass V B

Unconditional l1 error bound for the standard Perron line and height.

theorem MathlibNt.SieveTheory.LiuWeight.exists_liuPanPerronHyperbolaSum_eq_standardIntegral_add_error {q : ℕ} (U V : Finset ℕ) (A B : ℕ → ℂ) (χ : DirichletCharacter ℂ q) {Y M : ℕ} (hM : 3 ≤ M) (hYM : Y ≤ M) : ∃ (E : ℂ), liuPanPerronHyperbolaSum U V A B χ Y = liuPanTruncatedPerronIntegral U V A B χ (liuPanPerronSigma M) (liuPanPerronHeight M) Y + E ∧ ‖E‖ ≤ 32 * Real.exp 2 / ↑M * liuPanPerronCoefficientMass U A * liuPanPerronCoefficientMass V B

The finite hyperbola sum has an unconditional truncated Perron representation with explicit product-of-l1-masses error.