MellinAnalysis

Mellin inversion and lower-contour estimates.

theorem CohnElkies.strip_exp_abs_log_abs_integrable {a : ℝ} (ha : 0 < a) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (-a * |x|) * |Real.log |x||) MeasureTheory.volume

The exponential strip weight times the absolute logarithm is integrable.