Theorem 10.9 — change of variables

Proved

Rudin.ch10_change_of_variables

by Lucas · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisintegration

Let $T$ be a one-to-one $C'$ -mapping of an open set $E \subseteq \mathbb{R}^k$ into $\mathbb{R}^k$ whose Jacobian determinant vanishes nowhere, and let $f$ be continuous with compact support contained in $T(E)$ . Then $\int_{\mathbb{R}^k} f(\mathbf{y})\,d\mathbf{y} = \int_E f(T(\mathbf{x}))\,|J_T(\mathbf{x})|\,d\mathbf{x}$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch10_forms

open Filter Topology MeasureTheory

Formal statement

namespace Rudin

/-- Rudin, Theorem 10.9 (change of variables): if `T` is a one-to-one `C'`-mapping of an open
set `E ⊆ ℝᵏ` into `ℝᵏ` whose Jacobian never vanishes, and `f` is continuous with compact
support contained in `T(E)`, then
`∫ f(y) dy = ∫_E f(T x) |J_T(x)| dx`. -/
theorem ch10_change_of_variables (k : ℕ) (E : Set (Fin k → ℝ)) (hE : IsOpen E)
    (T : (Fin k → ℝ) → (Fin k → ℝ)) (hT : ContDiffOn ℝ 1 T E) (hinj : Set.InjOn T E)
    (hJ : ∀ x ∈ E, jacobian T id x ≠ 0)
    (f : (Fin k → ℝ) → ℝ) (hf : Continuous f) (hsupp : HasCompactSupport f)
    (hsub : tsupport f ⊆ T '' E) :
    (∫ y, f y) = ∫ x in E, f (T x) * |jacobian T id x| := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 10, p. 252, Theorem 10.9

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $k \in \mathbb{N}$ , let $E \subseteq \mathbb{R}^k$ be open, let $T : \mathbb{R}^k\to\mathbb{R}^k$ be continuously differentiable of order $1$ on $E$ and injective on $E$ , and assume its Jacobian determinant

J_T(x) = \det\Bigl( D_s\bigl(v\mapsto T(v)_r\bigr)(x) \Bigr)_{r,s}

is nonzero at every $x \in E$ . Let $f : \mathbb{R}^k\to\mathbb{R}$ be continuous on all of $\mathbb{R}^k$ , with compact support, and with closed support contained in the image $T(E)$ . Then

\int_{\mathbb{R}^k} f(y)\,dy \;=\; \int_{E} f\bigl(T(x)\bigr)\,\bigl|J_T(x)\bigr|\,dx ,

both being Lebesgue integrals (the right-hand one over the set $E$ ), with the convention that a non-integrable integrand contributes $0$ . The absolute value of the Jacobian appears on the right, so orientation does not enter. The case $k=0$ is formally included.

Human review

Endorsed by Shuze Chen · Sep 14, 2026
Endorsed by Community (Bot) · Sep 14, 2026
Endorsed by Lucas · Sep 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph