Scaling the Euler--Mascheroni Gamma kernel

This file records the positive-dilation form of the logarithmic Gamma kernel needed in Abelian finite-part arguments.

theorem AnalyticNumberTheory.Mertens.integrableOn_complex_log_mul_exp_neg : MeasureTheory.IntegrableOn (fun (t : ℝ) => ↑(Real.log t) * ↑(Real.exp (-t))) (Set.Ioi 0) MeasureTheory.volume

The logarithmic Gamma kernel is Bochner integrable on the positive half-line.

theorem AnalyticNumberTheory.Mertens.complex_scaled_integral_exp_eq_one (ε : ℝ) (hε : 0 < ε) : ↑ε * ∫ (t : ℝ) in Set.Ioi 0, ↑(Real.exp (-(ε * t))) = 1

The positive-dilation exponential kernel has total mass 1 / ε.

theorem AnalyticNumberTheory.Mertens.integrableOn_complex_exp_neg_mul (ε : ℝ) (hε : 0 < ε) : MeasureTheory.IntegrableOn (fun (t : ℝ) => ↑(Real.exp (-(ε * t)))) (Set.Ioi 0) MeasureTheory.volume

Integrability of the positive-dilation exponential kernel.

theorem AnalyticNumberTheory.Mertens.integrableOn_complex_log_mul_exp_neg_mul (ε : ℝ) (hε : 0 < ε) : MeasureTheory.IntegrableOn (fun (t : ℝ) => ↑(Real.log t) * ↑(Real.exp (-(ε * t)))) (Set.Ioi 0) MeasureTheory.volume

Integrability of the scaled logarithmic Gamma kernel.

theorem AnalyticNumberTheory.Mertens.complex_scaled_integral_log_exp_eq_neg_eulerMascheroni (ε : ℝ) (hε : 0 < ε) : (↑ε * ∫ (t : ℝ) in Set.Ioi 0, ↑(Real.log t) * ↑(Real.exp (-(ε * t)))) + ↑(Real.log ε) = -↑Real.eulerMascheroniConstant

The logarithmic Gamma kernel after the dilation u = ε t.

The statement is complex-valued so that it can directly reuse the Gamma derivative calculation in Mertens.Abelian.