Derivative of K under the integral sign

Open

ContWeatherall.fderiv_homotopyOp

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 smooth, then $D(K\omega)(x)h=\int_0^1t^k\big(t\,(D\omega(tx)h)(x,\cdot)+\omega(tx)(h,\cdot)\big)\,dt$ .

Preamble

import Mathlib
import Definitions.Def_ContWeatherall_defs

open CategoryTheory ContinuousAlternatingMap
open scoped ContDiff

Formal statement

namespace ContWeatherall

/-- Differentiation under the integral sign for the radial homotopy operator. -/
theorem fderiv_homotopyOp {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) (x h : E) :
    fderiv ℝ (homotopyOp w) x h = ∫ t in (0 : ℝ)..1,
      t ^ k • (t • (fderiv ℝ w (t • x) h).curryLeft x + (w (t • x)).curryLeft h) := by
  sorry

end ContWeatherall

Source

M. Spivak, Calculus on Manifolds (W. A. Benjamin, 1965), Theorem 4-11 (Poincaré lemma) and its proof (differentiation under the integral sign)

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}$ , $w:E\to\mathrm{Alt}^{k+1}(E;F)$ smooth, and $x,h\in E$ . Then the Fréchet derivative of $Kw$ at $x$ applied to $h$ is

D(Kw)(x)\,h=\int_0^1 t^k\Big(t\,\big(Dw(tx)h\big)(x,\cdot,\dots,\cdot)+w(tx)(h,\cdot,\dots,\cdot)\Big)\,dt\in\mathrm{Alt}^k(E;F),

where $Dw(tx)h\in\mathrm{Alt}^{k+1}(E;F)$ is the derivative of $w$ at $tx$ in direction $h$ , and $\alpha(x,\cdot)$ is first-slot contraction. For $k=0$ the factor $t^0=1$ .

View graph