@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 Oliveira1. 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 Fremlin2. This version generalizes readily to $n$ dimensions, but requires taking the absolute value of the derivative.
@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
is Lebesgue integrable, and the following identity holds:
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
By the Fundamental Theorem of Calculus
lemma FTC1,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) givesHence$F'(s) = G'(s)$ for a.e. $s \in [a, b]$ . Moreover,
By
lemma ae_eq_integralwe haveIn particular, evaluating at$s = b$ gives $F(b) = G(b)$ , i.e.,
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 Oliveira1. 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.$n$ dimensions, but requires taking the absolute value of the derivative.
Another measure-theoretic version can be found in the article by David Fremlin2. This version generalizes readily to
Footnotes
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). ↩
See Section 235 in https://www1.essex.ac.uk/maths/people/fremlin/chap23.pdf. ↩