Spivak Thm 4-11 (proof): K preserves smoothness

Open

ContWeatherall.homotopyOp_contDiff

by Alien60 · Oct 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

category-theorydifferential-formsgauge-theoryphilosophy-of-physicspoincare-lemma

Throughout, $E$ is a real normed space, $F$ a real normed space (Banach where stated), forms are Mathlib's E → E [⋀^Fin k]→L[ℝ] F, $d$ is extDeriv ( $d\omega(x)(v_0,\dots,v_k)=\sum_i(-1)^iD\omega(x)(v_i)(v_0,\dots,\widehat{v_i},\dots,v_k)$ ), smooth means ContDiff ℝ ∞, and $(K\omega)(x)(v)=\int_0^1t^k\,\omega(tx)(x,v)\,dt$ for a $(k+1)$ -form $\omega$ . If $F$ is complete and $\omega$ is a smooth $(k+1)$ -form, then $K\omega$ is a smooth $k$ -form.

Preamble

import Mathlib
import Definitions.Def_ContWeatherall_defs

open CategoryTheory ContinuousAlternatingMap
open scoped ContDiff

Formal statement

namespace ContWeatherall

/-- The radial homotopy operator maps smooth forms to smooth forms. -/
theorem homotopyOp_contDiff {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {k : ℕ} {w : E → E [⋀^Fin (k + 1)]→L[ℝ] F}
    (hw : ContDiff ℝ ∞ w) : ContDiff ℝ ∞ (homotopyOp w) := by
  sorry

end ContWeatherall

Source

M. Spivak, Calculus on Manifolds (W. A. Benjamin, 1965), Theorem 4-11 (Poincaré lemma) and its proof (I ω is a C^∞ form)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $E,F$ be real normed spaces with $F$ complete, $k\in\mathbb{N}$ , and $w:E\to\mathrm{Alt}^{k+1}(E;F)$ smooth ( $C^\infty$ ). Then $Kw:E\to\mathrm{Alt}^{k}(E;F)$ , $(Kw)(x)=\int_0^1 t^k\,w(tx)(x,\cdot,\dots,\cdot)\,dt$ , is smooth ( $C^\infty$ ).

View graph