Substitution formula for one-demensional Lebesgue integral

[Yosuke-Ito-345]

@affeldt-aist @t6s @IshiguroYoshihiro

As I mentioned here, I am formalizing a substitution (change-of-variables) formula for Lebesgue integral. Here is the blueprint.

Theorem

Let $a, b \in \mathbb{R}$ with $a \leq b$. Let $f : [a, b] \to \mathbb{R}$ be of class $C^1$, and let $g : \mathbb{R} \to \mathbb{R}$ be a bounded Borel measurable function. Then

$$(g \circ f) \cdot f' : [a, b] \to \mathbb{R}; \quad t \mapsto g(f(t)) \cdot f'(t)$$

is Lebesgue integrable, and the following identity holds:

$$\int_{f(a)}^{f(b)} g(x) \, dx = \int_a^b g(f(t)) f'(t) \, dt.$$

Here both sides are oriented Lebesgue integrals (i.e. sign is taken into account).

Proof

Since $g$ is bounded, $g \circ f$ is also bounded. Moreover, since $f$ is $C^1$ on $[a, b]$, $f'$ is continuous on $[a, b]$, hence in particular bounded and Borel measurable. Therefore $(g \circ f) \cdot f'$ is Lebesgue integrable on $[a, b]$.

Define functions $F, G : [a, b] \to \mathbb{R}$ by

$$F(s) := \int_a^s g(f(t)) f'(t) \, dt,$$ $$G(s) := \int_{f(a)}^{f(s)} g(x) \, dx.$$

By the Fundamental Theorem of Calculus lemma FTC1,

$$F'(t) = g(f(t)) f'(t) \quad \text{for a.e.\ } t \in [a, b].$$

Furthermore, viewing $G$ as the composition of $s \mapsto f(s)$ and $r \mapsto \int_{f(a)}^{r} g$, an application of lemma FTC1 (with the chain rule for the derivative of the composite functions) gives

$$G'(s) = g(f(s)) f'(s) \quad \text{for a.e.\ } s \in [a, b].$$

Hence $F'(s) = G'(s)$ for a.e. $s \in [a, b]$. Moreover,

$$F(a) = G(a) = 0.$$

By lemma ae_eq_integral we have

$$F = G \quad \text{on\ } [a, b].$$

In particular, evaluating at $s = b$ gives $F(b) = G(b)$, i.e.,

$$\int_a^b g(f(t))\, f'(t)\, dt \;=\; \int_{f(a)}^{f(b)} g(x)\, dx.$$

Observation

I think the bottleneck is to introduce the oriented Lebesgue integral, which we have yet to formalize.

Disclaimer

The idea of the proof is inspired by Claude and ChatGPT, but I wrote down the proof and checked its accuracy by myself. Therefore, I am responsible for any trouble coming from this formalization.

Related Documents

There are many variants of the substitution formula, including those for the Riemann integral. A survey of these variations is written by Oswaldo Rio Branco de Oliveira¹. The proof above may be viewed as a minor adaptation of the Riemann integral case, carried out using the fundamental theorem of calculus for the Lebesgue integral.
Another measure-theoretic version can be found in the article by David Fremlin². This version generalizes readily to $n$ dimensions, but requires taking the absolute value of the derivative.

Footnotes

1. See arXiv (https://arxiv.org/abs/2502.12679) or the presentation slide (https://blogs.mat.ucm.es/meninas-symposium/wp-content/uploads/sites/101/2025/06/ChangeVariableTotal-Talk-Beamer2025.pdf). ↩

2. See Section 235 in https://www1.essex.ac.uk/maths/people/fremlin/chap23.pdf. ↩

[Yosuke-Ito-345]

If you have any suggestions, please let me know.

[affeldt-aist]

If I remember correctly, @IshiguroYoshihiro took a look at defining the oriented integral.

[Yosuke-Ito-345]

@affeldt-aist
Thank you for your suggestion.
@IshiguroYoshihiro
Is there any work in progress on the oriented integral?