Theorem 10.25 — integration and pullback

Proved

Rudin.ch10_pullback_integral

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

analysisdifferential-forms

If $\Phi$ is a $k$ -surface in $\mathbb{R}^m$ and $T$ is a $C'$ -mapping into $\mathbb{R}^n$ , then $\int_{T\circ\Phi}\omega = \int_\Phi \omega_T$ for every $k$ -form $\omega$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch10_forms

open Filter Topology MeasureTheory

Formal statement

namespace Rudin

/-- Rudin, Theorem 10.25: integrating a form over the image surface `T ∘ Φ` is the same as
integrating its pullback over `Φ`. -/
theorem ch10_pullback_integral (k m n : ℕ) (T : (Fin m → ℝ) → (Fin n → ℝ))
    (hT : ContDiff ℝ 1 T) (ω : KForm k n) (Φ : SimplexSurface k m) (hΦ : ContDiff ℝ 1 Φ.map) :
    integralOverSimplex ω ⟨T ∘ Φ.map⟩ = integralOverSimplex (pullback T ω) Φ := by sorry

end Rudin

Source

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

Read-back

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

Let $k,m,n \in \mathbb{N}$ , let $T : \mathbb{R}^m\to\mathbb{R}^n$ be continuously differentiable of order $1$ on all of $\mathbb{R}^m$ , let $\omega$ be a $k$ -form in $\mathbb{R}^n$ (arbitrary coefficient functions, no regularity assumed), and let $\Phi$ be a simplex $k$ -surface in $\mathbb{R}^m$ that is continuously differentiable of order $1$ . Then

\int_{T\circ\Phi} \omega \;=\; \int_{\Phi} \omega_T ,

where on the left the composite $T \circ \Phi$ is regarded as a simplex $k$ -surface in $\mathbb{R}^n$ , and on the right $\omega_T$ is the pullback form with coefficients $\sum_i a_i(T(x)) \prod_r D_{j_r}\bigl(v\mapsto T(v)_{i_r}\bigr)(x)$ . Both sides are integrals over the standard simplex $Q^k$ of the corresponding sum of coefficient-times-Jacobian terms.

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