Prove2Me

Stokes' formula on the standard simplex Qk+1Q^{k+1}

Proved
Rudin.ch10_stokes_simplex

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

analysisdifferential-forms

Stokes' formula on the standard simplex, the analytic core of Rudin's Theorem 10.33.

Let k≥0k\ge 0 and let

ω=∑i1,…,ikai1⋯ik dxi1∧⋯∧dxik\omega = \sum_{i_1,\dots,i_k} a_{i_1\cdots i_k}\,dx_{i_1}\wedge\cdots\wedge dx_{i_k}

be a kk-form in Rk+1\mathbb{R}^{k+1} whose coefficient functions are of class C′C' on all of Rk+1\mathbb{R}^{k+1}. Let σ\sigma denote the oriented affine simplex [0,e1,…,ek+1][\mathbf{0},\mathbf{e}_1,\dots,\mathbf{e}_{k+1}], i.e. the (k+1)(k+1)-surface with parameter domain Qk+1Q^{k+1} given by the identity map of Qk+1Q^{k+1} (the affine map u↦∑iuieiu\mapsto \sum_i u_i\mathbf{e}_i is the identity). Then

∫σdω=∫∂σω,\int_\sigma d\omega = \int_{\partial\sigma}\omega,

where \partial\sigma=\sum_{j=0}^{k+1}(-1)^j\,\sigma\circ(\text{j-th face}) is the boundary kk-chain of Rudin's Definition 10.30, obtained by deleting the jj-th vertex of [0,e1,…,ek+1][\mathbf{0},\mathbf{e}_1,\dots,\mathbf{e}_{k+1}].

This is exactly the computation Rudin carries out on pp. 273-274: after expanding the Jacobian of the identity along the index tuples, the left-hand side becomes an integral over Qk+1Q^{k+1} of a signed sum of first-order partial derivatives of the coefficients, and the fundamental theorem of calculus applied in each coordinate direction, together with the iterated-integral theorem, converts it into the alternating sum of the integrals over the k+2k+2 faces of Qk+1Q^{k+1}.

Every other ingredient of Stokes' theorem for a general chain is formal: a chain is integrated term by term, a general (m+1)(m+1)-surface Φ\Phi is reduced to this case by pulling ω\omega back along Φ\Phi (Rudin's Theorems 10.22(c) and 10.25), and the faces of Φ\Phi are the composites of Φ\Phi with the faces of Qm+1Q^{m+1}.

Preamble
import Mathlib
import Definitions.Def_Rudin_ch10_forms

open Filter Topology MeasureTheory
Formal statement
namespace Rudin

/-- Rudin, Theorem 10.33 (Stokes' theorem), the case of the identity surface of the standard
simplex: if `ω` is a `k`-form of class `C'` in `ℝ^{k+1}`, then the integral of `dω` over the
oriented simplex `Q^{k+1}` equals the integral of `ω` over its boundary chain. -/
theorem ch10_stokes_simplex (k : ℕ) (ω : KForm k (k + 1)) (hω : ∀ i, ContDiff ℝ 1 (ω.coeff i)) :
    integralOverSimplex (extDeriv ω) ⟨id⟩ = Chain.integral ω (surfaceBoundary ⟨id⟩) := by sorry

end Rudin
Source
Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 10, Theorem 10.33 (Stokes' theorem), pp. 273-274 (the case of the oriented affine simplex [0, e_1, ..., e_{k+1}]), together with Definition 10.30 (boundary of a surface)

View graph