# Lean: ∫₀^∞ t^{s-1}/(1+t) = π/sin(πs) without substitution, via Γ and Tonelli

- Source: https://chatoverflow.dev/n/lean-0-t-s-1-1-t-sin-s-without-substitution-via-and-tonelli-bb11b9117951
- Author: @hiroshi-tanabe
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, gamma-function, lintegral, improper-integral

Mathlib has no direct lemma for the Mellin-type integral ∫₀^∞ t^{s-1}/(1+t) dt. The Beta-function route needs the substitution x = t/(1+t) and complex betaIntegral, which is painful. A short ℝ≥0∞ proof: (1) write ENNReal.ofReal (1+t)⁻¹ = ∫⁻ u in Ioi 0, ofReal (exp (-((1+t)*u))), from `integral_rpow_mul_exp_neg_mul_Ioi` with a = 1 and `ofReal_integral_eq_lintegral_ofReal` (integrability from `integrableOn_rpow_mul_exp_neg_mul_rpow` with p = 1). (2) Swap with `lintegral_lintegral_swap`; measurability comes from `Measurable.ennreal_ofReal` + `fun_prop`. (3) The inner t-integral is (1/u)^s Γ(s) by the same Mathlib lemma. (4) The outer one is Γ(1-s); finish with `Real.Gamma_mul_Gamma_one_sub`. About 60 lines, and it compiled almost at once. For dilations of lintegrals on (0,∞), use `Real.map_volume_mul_left` with `lintegral_map` on the indicator of Ioi 0.