Theorem 10.39 — Poincaré's lemma

Proved

Rudin.ch10_poincare_lemma

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

analysisdifferential-forms

If $E \subseteq \mathbb{R}^n$ is convex and open and $\omega$ is a closed $k$ -form of class $C'$ in $E$ with $k \ge 1$ , then $\omega$ is exact: $\omega = d\eta$ for some $(k-1)$ -form $\eta$ of class $C'$ in $E$ . Closedness and exactness are stated through integrals over surfaces contained in $E$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch10_forms

open Filter Topology MeasureTheory

Formal statement

namespace Rudin

/-- Rudin, Theorem 10.39 (Poincaré's lemma): on a convex open set every closed form of positive
order and class `C'` is exact.  Closedness and exactness are expressed through integrals over
surfaces lying in `E`, since a form is determined by those integrals. -/
theorem ch10_poincare_lemma (m n : ℕ) (E : Set (Fin n → ℝ)) (hE : IsOpen E) (hconv : Convex ℝ E)
    (ω : KForm (m + 1) n) (hω : ∀ i, ContDiffOn ℝ 1 (ω.coeff i) E)
    (hclosed : ∀ Φ : SimplexSurface (m + 1 + 1) n, ContDiff ℝ 1 Φ.map →
      (∀ u, Φ.map u ∈ E) → integralOverSimplex (extDeriv ω) Φ = 0) :
    ∃ η : KForm m n, (∀ i, ContDiffOn ℝ 1 (η.coeff i) E) ∧
      ∀ Φ : SimplexSurface (m + 1) n, ContDiff ℝ 1 Φ.map → (∀ u, Φ.map u ∈ E) →
        integralOverSimplex ω Φ = integralOverSimplex (extDeriv η) Φ := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 10, p. 278, Definition 10.34 and Theorem 10.39

Read-back

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

Let $m,n \in \mathbb{N}$ , let $E \subseteq \mathbb{R}^n$ be open and convex, and let $\omega$ be an $(m+1)$ -form in $\mathbb{R}^n$ (so of order at least $1$ ) whose coefficient functions are all continuously differentiable of order $1$ on $E$ . Assume $\omega$ is closed in the integral sense: for every simplex $(m+2)$ -surface $\Phi$ that is continuously differentiable of order $1$ and whose map sends every point of $\mathbb{R}^{m+2}$ into $E$ , one has $\int_{\Phi} d\omega = 0$ .

Then there exists an $m$ -form $\eta$ in $\mathbb{R}^n$ such that:

all coefficients of $\eta$ are continuously differentiable of order $1$ on $E$ ;
for every simplex $(m+1)$ -surface $\Phi$ that is continuously differentiable of order $1$ with image contained in $E$ (again, the map sends all of $\mathbb{R}^{m+1}$ into $E$ ),

\int_{\Phi} \omega \;=\; \int_{\Phi} d\eta .

Note that the containment condition is imposed on the whole map, not only on its restriction to the standard simplex $Q^{m+1}$ , which restricts the class of test surfaces; exactness is asserted only through equality of integrals over such surfaces, 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