Theorem 10.20 — $d(d\omega) = 0$

Proved

Rudin.ch10_dd_zero

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

analysisdifferential-forms

If $\omega$ is a $k$ -form of class $C''$ , then $d(d\omega) = 0$ : the integral of $d(d\omega)$ over every $(k+2)$ -surface is zero.

Preamble

import Mathlib
import Definitions.Def_Rudin_ch10_forms

open Filter Topology MeasureTheory

Formal statement

namespace Rudin

/-- Rudin, Theorem 10.20: `d(dω) = 0` for every form `ω` of class `C''`; as forms are
functionals on surfaces, this says that the integral of `d(dω)` over every surface vanishes. -/
theorem ch10_dd_zero (k n : ℕ) (ω : KForm k n) (hω : ∀ i, ContDiff ℝ 2 (ω.coeff i))
    (Φ : SimplexSurface (k + 2) n) (hΦ : ContDiff ℝ 1 Φ.map) :
    integralOverSimplex (extDeriv (extDeriv ω)) Φ = 0 := by sorry

end Rudin

Source

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

Read-back

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

Let $k, n \in \mathbb{N}$ and let $\omega$ be a $k$ -form in $\mathbb{R}^n$ (a coefficient function $a_i : \mathbb{R}^n\to\mathbb{R}$ for every index tuple $i$ ) all of whose coefficients are twice continuously differentiable on all of $\mathbb{R}^n$ . Let $\Phi$ be a simplex $(k+2)$ -surface, i.e. a map $\mathbb{R}^{k+2}\to\mathbb{R}^n$ , which is continuously differentiable of order $1$ . Then

\int_{\Phi} d(d\omega) \;=\; 0,

that is, the number

\int_{Q^{k+2}} \sum_{i} \bigl(d(d\omega)\bigr)_i\bigl(\Phi(u)\bigr)\, J_i\Phi(u)\, du

is zero, the sum running over all index tuples $i : \{1,\dots,k+2\}\to\{0,\dots,n-1\}$ , the integral being over the standard simplex $Q^{k+2}$ , and $d$ being the exterior derivative that differentiates each coefficient in the direction named by the first index.

The vanishing is asserted for this one surface integral (for every such $\Phi$ , since $\Phi$ is universally quantified), not as an identity of coefficient functions.

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

Theorem 10.20 — d(dω)=0d(d\omega) = 0d(dω)=0

Theorem 10.20 — $d(d\omega) = 0$