Inversion r = c/δ in a lower Lebesgue integral with weight dr/r

Proved

DbarRegularity.lintegral_Ici_comp_div_mul_inv

by Mazecto · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

measure-theoryreal-analysis

Let $c>0$ and let $w:\mathbb{R}\to[0,\infty]$ be any function. Then

\int_{r\ge c} w\!\left(\frac{c}{r}\right)\frac{dr}{r}\;=\;\int_{0<\delta\le1} w(\delta)\,\frac{d\delta}{\delta},

both sides being lower Lebesgue integrals with values in $[0,\infty]$ .

Formalization Note. The integrals are ∫⁻ over Ici c and Ioc 0 1 for Lebesgue measure; $1/r$ is (ENNReal.ofReal r)⁻¹. No measurability of $w$ is assumed.

Preamble

import Mathlib.MeasureTheory.Function.JacobianOneDim
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.Calculus.Deriv.Inv

Formal statement

namespace DbarRegularity

open MeasureTheory Set
open scoped ENNReal

/-- For `c > 0` and any `w : ℝ → [0, ∞]`:
`∫_{r ≥ c} w(c / r) dr / r = ∫_{0 < δ ≤ 1} w(δ) dδ / δ`. -/
theorem lintegral_Ici_comp_div_mul_inv {c : ℝ} (hc : 0 < c) (w : ℝ → ℝ≥0∞) :
    ∫⁻ r in Ici c, w (c / r) * (ENNReal.ofReal r)⁻¹ =
      ∫⁻ δ in Ioc (0 : ℝ) 1, w δ * (ENNReal.ofReal δ)⁻¹ := by sorry

end DbarRegularity

Source

E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Princeton Mathematical Series 30, Princeton University Press (1970), Chapter II, § 4.2, Theorem 3, p. 39

View graph