An Abelian remainder estimate

This file isolates the dominated-convergence argument used after the logarithmic change of variables in Mertens' theorem. A fixed positive cutoff avoids imposing artificial hypotheses at the origin.

theorem AnalyticNumberTheory.Mertens.mul_exp_neg_mul_le_inv {ε u : ℝ} (hε : 0 < ε) (hu : 0 < u) : ε * Real.exp (-(ε * u)) ≤ u⁻¹

The elementary uniform estimate behind the Abelian remainder argument.

theorem AnalyticNumberTheory.Mertens.tendsto_mul_integral_exp_remainder_of_integrable_norm_div {E : ℝ → ℂ} {a : ℝ} (ha : 0 < a) (hE : MeasureTheory.AEStronglyMeasurable E (MeasureTheory.volume.restrict (Set.Ioi a))) (hdiv : MeasureTheory.IntegrableOn (fun (u : ℝ) => ‖E u‖ / u) (Set.Ioi a) MeasureTheory.volume) : Filter.Tendsto (fun (ε : ℝ) => ↑ε * ∫ (u : ℝ) in Set.Ioi a, E u * ↑(Real.exp (-(ε * u)))) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

A reusable Abelian remainder lemma on a half-line with positive cutoff.

The weighted integrability assumption is exactly what is supplied by local integrability together with an eventual O(1/u) estimate: on compact pieces division by u is harmless, while on the tail it gives an integrable O(1/u^2) majorant.

theorem AnalyticNumberTheory.Mertens.integrableOn_norm_div_of_compact_of_inv_tail {E : ℝ → ℂ} {a A C : ℝ} (ha : 0 < a) (haA : a ≤ A) (hcompact : MeasureTheory.IntegrableOn (fun (u : ℝ) => ‖E u‖ / u) (Set.Ioc a A) MeasureTheory.volume) (hmeas : MeasureTheory.AEStronglyMeasurable (fun (u : ℝ) => ‖E u‖ / u) (MeasureTheory.volume.restrict (Set.Ioi A))) (htail : ∀ u ∈ Set.Ioi A, ‖E u‖ ≤ C / u) : MeasureTheory.IntegrableOn (fun (u : ℝ) => ‖E u‖ / u) (Set.Ioi a) MeasureTheory.volume

Local weighted integrability plus an explicit C/u tail bound gives the global weighted integrability needed by the Abelian remainder lemma.

theorem AnalyticNumberTheory.Mertens.tendsto_mul_integral_exp_remainder_of_inv_tail {E : ℝ → ℂ} {a A C : ℝ} (ha : 0 < a) (haA : a ≤ A) (hE : MeasureTheory.AEStronglyMeasurable E (MeasureTheory.volume.restrict (Set.Ioi a))) (hcompact : MeasureTheory.IntegrableOn (fun (u : ℝ) => ‖E u‖ / u) (Set.Ioc a A) MeasureTheory.volume) (hmeas : MeasureTheory.AEStronglyMeasurable (fun (u : ℝ) => ‖E u‖ / u) (MeasureTheory.volume.restrict (Set.Ioi A))) (htail : ∀ u ∈ Set.Ioi A, ‖E u‖ ≤ C / u) : Filter.Tendsto (fun (ε : ℝ) => ↑ε * ∫ (u : ℝ) in Set.Ioi a, E u * ↑(Real.exp (-(ε * u)))) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The practical cutoff form: a compact initial piece and an eventual C/u estimate imply that the exponentially damped remainder vanishes in the Abelian limit ε → 0+.