Logarithmic change of variables for the prime Abel integral

This file records the substitution x = exp u in the integral occurring in primeDirichletSum_eq_mul_integral_of_pos. The Jacobian cancels the extra factor x⁻¹, leaving the exponential Abel kernel exp (-εu).

theorem AnalyticNumberTheory.Mertens.primeAbel_integral_log_change (ε : ℝ) (_hε : 0 < ε) : ∫ (x : ℝ) in Set.Ioi 1, ↑(primeReciprocalSum ⌊x⌋₊) * ↑x ^ (-(↑ε + 1)) = ∫ (u : ℝ) in Set.Ioi 0, ↑(primeReciprocalSum ⌊Real.exp u⌋₊) * ↑(Real.exp (-(ε * u)))

The logarithmic change of variables x = exp u for the prime Abel integral. No separate integrability assumption is needed: this is the unconditional change-of-variables identity for the Bochner integral used by Mathlib.