Chen 1973, Lemma 1: the literal finite Mellin--Perron kernel

This file formalizes the exact finite formula obtained after the Bromwich contour calculation on pp. 112--113 of Chen's 1973 paper. It is deliberately independent of the truncated sine Perron kernel elsewhere in this repository.

For n = ⌊log x⌋ and t = (log x)^(11/10) log y, Chen obtains, for y ≥ 1,

Φ(y) = 1 - exp (-t) * ∑ ν = 0..n, t^ν / ν!

and identifies this with the normalized integral

1 / n! * ∫ λ in 0..t, exp (-λ) λ^n dλ.

The definition below remains honestly named ...Finite: its identification with Mathlib's Bochner integral over the full vertical line is proved in the companion module Chen1973Lemma1MellinClosure, which supplies the unconditional Chen1973BromwichIdentity.

noncomputable def AnalyticNumberTheory.LargeSieve.chenExpPartial (n : ℕ) (t : ℝ) : ℝ

The finite exponential polynomial ∑_{ν=0}^n t^ν / ν!.

Equations

• AnalyticNumberTheory.LargeSieve.chenExpPartial n t = ∑ ν ∈ Finset.range (n + 1), t ^ ν / ↑ν.factorial

@[simp]

theorem AnalyticNumberTheory.LargeSieve.chenExpPartial_zero (t : ℝ) : chenExpPartial 0 t = 1

@[simp]

theorem AnalyticNumberTheory.LargeSieve.chenExpPartial_at_zero (n : ℕ) : chenExpPartial n 0 = 1

noncomputable def AnalyticNumberTheory.LargeSieve.chenGammaCDF (n : ℕ) (t : ℝ) : ℝ

The source's post-contour normalized Gamma-CDF formula.

Equations

• AnalyticNumberTheory.LargeSieve.chenGammaCDF n t = 1 - Real.exp (-t) * AnalyticNumberTheory.LargeSieve.chenExpPartial n t

@[simp]

theorem AnalyticNumberTheory.LargeSieve.chenGammaCDF_zero (n : ℕ) : chenGammaCDF n 0 = 0

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973PerronScale (x : ℝ) : ℝ

Literal source scale (log x)^1.1, written without decimal notation.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973PerronScale x = Real.log x ^ (11 / 10)

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973PerronOrder (x : ℝ) : ℕ

Literal integer parameter [log x] from Chen 1973.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973PerronOrder x = ⌊Real.log x⌋₊

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973PerronKernelFinite (x y : ℝ) : ℝ

Chen's Lemma 1 kernel in its exact finite, post-contour form. The branch at y ≤ 1 is the source's strict Perron cutoff; for y > 1 this is the finite Gamma-CDF/exponential-sum formula printed on p. 113.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973PerronKernelFinite x y = if y ≤ 1 then 0 else AnalyticNumberTheory.LargeSieve.chenGammaCDF (AnalyticNumberTheory.LargeSieve.chen1973PerronOrder x) (AnalyticNumberTheory.LargeSieve.chen1973PerronScale x * Real.log y)

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973BromwichIntegrand (x y t : ℝ) : ℂ

The literal complex integrand on the vertical line Re ω = 2. This is data only; no convergence or contour-shift theorem is asserted here.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973BromwichIntegrand x y t = (↑y).cpow (2 + ↑t * Complex.I) / ((2 + ↑t * Complex.I) * (1 + (2 + ↑t * Complex.I) / ↑(AnalyticNumberTheory.LargeSieve.chen1973PerronScale x)) ^ (AnalyticNumberTheory.LargeSieve.chen1973PerronOrder x + 1))

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973GammaDensityPrimitive (x r : ℝ) : ℂ

The compactly supported Gamma primitive whose Mellin transform is Chen's rational Bromwich kernel. The endpoint value at r = 1 is zero because chenGammaCDF n 0 = 0.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973GammaDensityPrimitive x r = if r ≤ 0 ∨ 1 ≤ r then 0 else ↑(AnalyticNumberTheory.LargeSieve.chenGammaCDF (AnalyticNumberTheory.LargeSieve.chen1973PerronOrder x) (AnalyticNumberTheory.LargeSieve.chen1973PerronScale x * Real.log (1 / r)))

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973MellinKernel (x : ℝ) (s : ℂ) : ℂ

The rational function occurring as the Mellin transform of chen1973GammaDensityPrimitive.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973MellinKernel x s = 1 / (s * (1 + s / ↑(AnalyticNumberTheory.LargeSieve.chen1973PerronScale x)) ^ (AnalyticNumberTheory.LargeSieve.chen1973PerronOrder x + 1))

theorem AnalyticNumberTheory.LargeSieve.chen1973GammaDensityPrimitive_one_div {x y : ℝ} (hy : 0 < y) : chen1973GammaDensityPrimitive x (1 / y) = ↑(chen1973PerronKernelFinite x y)

Evaluation of the Gamma primitive at the reciprocal variable recovers the literal finite Perron kernel, including the source cutoff 0 < y ≤ 1.

theorem AnalyticNumberTheory.LargeSieve.verticalIntegrable_chen1973MellinKernel {x : ℝ} (hx : 1 < x) : Complex.VerticalIntegrable (chen1973MellinKernel x) 2 MeasureTheory.volume

The rational Mellin kernel is integrable on Chen's vertical line.

theorem AnalyticNumberTheory.LargeSieve.mellinInv_chen1973MellinKernel_eq_bromwich {x y : ℝ} (hy : 0 < y) : mellinInv 2 (chen1973MellinKernel x) (1 / y) = ↑(1 / (2 * Real.pi)) * ∫ (t : ℝ), chen1973BromwichIntegrand x y t

Parameterizing the inverse Mellin transform on re s = 2 gives Chen's real-line Bromwich integral.

theorem AnalyticNumberTheory.LargeSieve.chen1973BromwichIdentity_of_mellin (x : ℝ) (hx : 1 < x) (hMellin : ∀ (s : ℂ), s.re = 2 → mellin (chen1973GammaDensityPrimitive x) s = chen1973MellinKernel x s) (hconv : MellinConvergent (chen1973GammaDensityPrimitive x) 2) (hcont : ∀ (r : ℝ), 0 < r → ContinuousAt (chen1973GammaDensityPrimitive x) r) (y : ℝ) : 0 < y → ↑(1 / (2 * Real.pi)) * ∫ (t : ℝ), chen1973BromwichIntegrand x y t = ↑(chen1973PerronKernelFinite x y)

Mellin inversion specialized to Chen's Gamma primitive, with its three analytic premises exposed. Chen1973Lemma1MellinClosure discharges these premises and publishes the unconditional Chen1973BromwichIdentity.

@[simp]

theorem AnalyticNumberTheory.LargeSieve.chen1973PerronKernelFinite_of_le_one {x y : ℝ} (hy : y ≤ 1) : chen1973PerronKernelFinite x y = 0

@[simp]

theorem AnalyticNumberTheory.LargeSieve.chen1973PerronKernelFinite_zero (x : ℝ) : chen1973PerronKernelFinite x 0 = 0

theorem AnalyticNumberTheory.LargeSieve.chen1973PerronKernelFinite_of_one_lt {x y : ℝ} (hy : 1 < y) : chen1973PerronKernelFinite x y = 1 - Real.exp (-(chen1973PerronScale x * Real.log y)) * ∑ ν ∈ Finset.range (chen1973PerronOrder x + 1), (chen1973PerronScale x * Real.log y) ^ ν / ↑ν.factorial

Chen's printed finite exponential-sum identity on the y > 1 branch.

theorem AnalyticNumberTheory.LargeSieve.one_sub_chenGammaCDF (n : ℕ) (t : ℝ) : 1 - chenGammaCDF n t = Real.exp (-t) * chenExpPartial n t

The complementary tail is exactly Chen's finite exponential sum.

theorem AnalyticNumberTheory.LargeSieve.chenGammaCDF_succ (n : ℕ) (t : ℝ) : chenGammaCDF (n + 1) t = chenGammaCDF n t - Real.exp (-t) * t ^ (n + 1) / ↑(n + 1).factorial

Recurrence obtained by peeling off the final term of the finite exponential sum.

theorem AnalyticNumberTheory.LargeSieve.hasDerivAt_chenGammaCDF (n : ℕ) (t : ℝ) : HasDerivAt (chenGammaCDF n) (Real.exp (-t) * t ^ n / ↑n.factorial) t

The derivative of the finite Gamma CDF is its normalized Gamma density.

theorem AnalyticNumberTheory.LargeSieve.chenGammaCDF_eq_intervalIntegral (n : ℕ) (t : ℝ) : chenGammaCDF n t = 1 / ↑n.factorial * ∫ (u : ℝ) in 0..t, Real.exp (-u) * u ^ n

Chen's finite formula equals the normalized interval Gamma integral exactly.

theorem AnalyticNumberTheory.LargeSieve.chenGammaCDF_monotoneOn (n : ℕ) : MonotoneOn (chenGammaCDF n) (Set.Ici 0)

The finite Gamma CDF is monotone on its source range.

theorem AnalyticNumberTheory.LargeSieve.chenExpPartial_nonneg (n : ℕ) {t : ℝ} (ht : 0 ≤ t) : 0 ≤ chenExpPartial n t

Every term in Chen's finite exponential polynomial is nonnegative for t ≥ 0.

theorem AnalyticNumberTheory.LargeSieve.chenExpPartial_le_exp (n : ℕ) {t : ℝ} (ht : 0 ≤ t) : chenExpPartial n t ≤ Real.exp t

The exponential Taylor lower bound controls the finite polynomial.

theorem AnalyticNumberTheory.LargeSieve.chenExpPartial_le_two_pow_mul_exp_half (n : ℕ) {t : ℝ} (ht : 0 ≤ t) : chenExpPartial n t ≤ 2 ^ n * Real.exp (t / 2)

A convenient exponentially decaying majorant for Chen's finite tail.

theorem AnalyticNumberTheory.LargeSieve.one_sub_chenGammaCDF_le_two_pow_mul_exp_neg_half (n : ℕ) {t : ℝ} (ht : 0 ≤ t) : 1 - chenGammaCDF n t ≤ 2 ^ n * Real.exp (-t / 2)

The complementary CDF tail is at most 2^n exp (-t/2) for t ≥ 0.

theorem AnalyticNumberTheory.LargeSieve.chenGammaCDF_mem_Icc (n : ℕ) {t : ℝ} (ht : 0 ≤ t) : chenGammaCDF n t ∈ Set.Icc 0 1

The Gamma-CDF finite formula lies in [0,1] on the source range t ≥ 0.

theorem AnalyticNumberTheory.LargeSieve.chenGammaCDF_tail_mem_Icc (n : ℕ) {t : ℝ} (ht : 0 ≤ t) : 1 - chenGammaCDF n t ∈ Set.Icc 0 1

Exact two-sided tail enclosure furnished by the finite source formula.

theorem AnalyticNumberTheory.LargeSieve.chen1973PerronArgument_nonneg {x y : ℝ} (hx : 1 < x) (hy : 1 ≤ y) : 0 ≤ chen1973PerronScale x * Real.log y

Source-range positivity of the transformed coordinate.

theorem AnalyticNumberTheory.LargeSieve.chen1973PerronKernelFinite_mem_Icc {x y : ℝ} (hx : 1 < x) (_hy : 0 ≤ y) : chen1973PerronKernelFinite x y ∈ Set.Icc 0 1

Consequently the literal finite kernel is between zero and one.

theorem AnalyticNumberTheory.LargeSieve.chen1973PerronKernelFinite_monotoneOn {x : ℝ} (hx : 1 < x) : MonotoneOn (chen1973PerronKernelFinite x) (Set.Ici 0)

For fixed x > 1, Chen's finite kernel is monotone on nonnegative inputs.

theorem AnalyticNumberTheory.LargeSieve.chen1973PerronKernelFinite_lower_bound {x y : ℝ} (hx1 : 1 < x) (hx : 10 ^ 7 ≤ Real.log x) (hy : Real.exp (2 * Real.log x ^ (-1 / 10)) ≤ y) : 1 - x ^ (-1 / 10) ≤ chen1973PerronKernelFinite x y

Chen's explicit lower bound in the original numerical range. The proof is purely analytic: the finite tail is bounded by 2^n exp (-t/2), then n = ⌊log x⌋ ≤ log x, log 2 < 9/10, and t ≥ 2 log x give the result.