The differential--delay equation for Suzuki's standard upper adjoint

This module proves the equation from the defining Laplace integral. In particular, the differential--delay equation is not used as an assumption.

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

A first exponential moment remains integrable after inserting Suzuki's nonnegative Ein weight.

theorem MathlibNt.SieveTheory.hasDerivAt_suzukiStandardUpperAdjoint_integral {s : ℝ} (hs : 0 < s) : HasDerivAt suzukiStandardUpperAdjoint (∫ (x : ℝ) in Set.Ioi 0, -x * Real.exp (-s * x - suzukiEin x)) s

Differentiation under the defining improper integral, proved by a local integrable majorant.

theorem MathlibNt.SieveTheory.hasDerivAt_suzukiStandardUpperAdjoint_moment {s : ℝ} (hs : 0 < s) : HasDerivAt suzukiStandardUpperAdjoint (-∫ (x : ℝ) in Set.Ioi 0, x * Real.exp (-s * x - suzukiEin x)) s

The exact derivative before identifying the first moment with a delayed value.

theorem MathlibNt.SieveTheory.hasDerivAt_mul_standardUpperAdjoint_integrand (s x : ℝ) : HasDerivAt (fun (y : ℝ) => y * Real.exp (-s * y - suzukiEin y)) (Real.exp (-(s + 1) * x - suzukiEin x) - s * (x * Real.exp (-s * x - suzukiEin x))) x

The finite-interval integration-by-parts identity producing the delay.

theorem MathlibNt.SieveTheory.standardUpperAdjoint_moment_identity {s : ℝ} (hs : 0 < s) : s * ∫ (x : ℝ) in Set.Ioi 0, x * Real.exp (-s * x - suzukiEin x) = suzukiStandardUpperAdjoint (s + 1)

The x-moment of the defining kernel is exactly the shifted adjoint divided by the Laplace parameter.

theorem MathlibNt.SieveTheory.suzukiStandardUpperAdjoint_hasDerivAt_dde {s : ℝ} (hs : 0 < s) : HasDerivAt suzukiStandardUpperAdjoint (-suzukiStandardUpperAdjoint (s + 1) / s) s

Suzuki's standard upper adjoint satisfies its adjoint differential--delay equation on the positive half-line.