Suzuki's standard upper adjoint r_{1,-1}

Suzuki §10 defines, when a+b<1,

r_{a,b}(s) = 1 / Γ(1-a-b) * ∫ x in (0,∞), exp (-s*x + b*Ein(x)) * x^(-(a+b)).

Thus the standard upper adjoint is

r_{1,-1}(s) = ∫ x in (0,∞), exp (-s*x - Ein(x)).

This module starts its source-faithful construction. It defines the removable kernel (1-exp(-x))/x, its primitive Ein, and the genuine Laplace integral. It closes the local identities which drive both remaining endpoints:

• differentiation under the Laplace integral gives p'(s)=-p(s+1)/s;
• x * exp (-Ein x) is an exact primitive of the integrand defining p(1).

The latter reduces p(1)=exp(-γ) to the classical (non-Buchstab) asymptotic x * exp(-Ein x) → exp(-γ). No value at 1 is inserted by definition.

noncomputable def MathlibNt.SieveTheory.suzukiEinKernel : ℝ → ℝ

The continuous removable extension of (1 - exp (-x)) / x at zero.

Equations

• MathlibNt.SieveTheory.suzukiEinKernel = Function.update (fun (x : ℝ) => (1 - Real.exp (-x)) / x) 0 1

@[simp]

theorem MathlibNt.SieveTheory.suzukiEinKernel_zero : suzukiEinKernel 0 = 1

theorem MathlibNt.SieveTheory.suzukiEinKernel_of_ne {x : ℝ} (hx : x ≠ 0) : suzukiEinKernel x = (1 - Real.exp (-x)) / x

theorem MathlibNt.SieveTheory.continuous_suzukiEinKernel : Continuous suzukiEinKernel

The apparent singularity in Suzuki's Ein kernel is removable.

noncomputable def MathlibNt.SieveTheory.suzukiEin (x : ℝ) : ℝ

Suzuki's entire exponential integral on the real axis, Ein(x)=∫₀ˣ (1-exp(-t))/t dt, using the removable value at zero.

Equations

• MathlibNt.SieveTheory.suzukiEin x = ∫ (t : ℝ) in 0..x, MathlibNt.SieveTheory.suzukiEinKernel t

noncomputable def MathlibNt.SieveTheory.suzukiStandardUpperAdjoint (s : ℝ) : ℝ

The Laplace-integral construction of Suzuki's r_{1,-1}.

Equations

• MathlibNt.SieveTheory.suzukiStandardUpperAdjoint s = ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-s * x - MathlibNt.SieveTheory.suzukiEin x)

theorem MathlibNt.SieveTheory.mul_suzukiEinKernel {x : ℝ} (hx : x ≠ 0) : x * suzukiEinKernel x = 1 - Real.exp (-x)

Away from the removable point, multiplying the Ein kernel by its argument recovers 1-exp(-x).

theorem MathlibNt.SieveTheory.mul_suzukiEinKernel_all (x : ℝ) : x * suzukiEinKernel x = 1 - Real.exp (-x)

theorem MathlibNt.SieveTheory.suzukiEinKernel_nonneg {x : ℝ} (hx : 0 ≤ x) : 0 ≤ suzukiEinKernel x

The removable kernel is nonnegative on the positive half-line.

theorem MathlibNt.SieveTheory.suzukiEin_nonneg {x : ℝ} (hx : 0 ≤ x) : 0 ≤ suzukiEin x

theorem MathlibNt.SieveTheory.hasDerivAt_suzukiEin {x : ℝ} : HasDerivAt suzukiEin (suzukiEinKernel x) x

A local calculus package sufficient for all source-faithful downstream arguments. Continuity is separated because it is exactly the removable singularity lemma, independent of the later improper integral.

theorem MathlibNt.SieveTheory.continuous_suzukiEin : Continuous suzukiEin

theorem MathlibNt.SieveTheory.integrableOn_standardUpperAdjoint_integrand {s : ℝ} (hs : 0 < s) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (-s * x - suzukiEin x)) (Set.Ioi 0) MeasureTheory.volume

The source integral defining r_{1,-1} is genuinely integrable for every positive Laplace parameter.

theorem MathlibNt.SieveTheory.suzukiStandardUpperAdjoint_pos {s : ℝ} (hs : 0 < s) : 0 < suzukiStandardUpperAdjoint s

Positivity of the standard adjoint follows from its positive Laplace kernel, not from an imposed initial value.

theorem MathlibNt.SieveTheory.hasDerivAt_mul_exp_neg_suzukiEin (x : ℝ) : HasDerivAt (fun (y : ℝ) => y * Real.exp (-suzukiEin y)) (Real.exp (-x - suzukiEin x)) x

Exact finite-interval primitive identity behind r_{1,-1}(1)=exp(-γ). This is the earliest normalization node and does not assume the desired value.

theorem MathlibNt.SieveTheory.integral_exp_neg_sub_suzukiEin_zero_to (R : ℝ) : ∫ (x : ℝ) in 0..R, Real.exp (-x - suzukiEin x) = R * Real.exp (-suzukiEin R)

Every finite truncation of the integral defining r_{1,-1}(1) is exactly the Euler--Ein boundary term.

def MathlibNt.SieveTheory.SuzukiEinEulerTailAsymptotic : Prop

The desired boundary value is reduced to the classical Euler--Ein tail asymptotic, rather than postulated as the definition of the adjoint.

Equations

• MathlibNt.SieveTheory.SuzukiEinEulerTailAsymptotic = Filter.Tendsto (fun (x : ℝ) => x * Real.exp (-MathlibNt.SieveTheory.suzukiEin x)) Filter.atTop (nhds (Real.exp (-Real.eulerMascheroniConstant)))

theorem MathlibNt.SieveTheory.suzukiStandardUpperAdjoint_one_eq_exp_neg_eulerMascheroni (htail : SuzukiEinEulerTailAsymptotic) : suzukiStandardUpperAdjoint 1 = Real.exp (-Real.eulerMascheroniConstant)

Once the classical Euler--Ein tail asymptotic is supplied, the actual Laplace integral (not a normalized placeholder) has Suzuki's required value.