Radial fundamental theorem of calculus

Open

ContWeatherall.integral_radial

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

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

For a $C^1$ map $g:E\to G$ into a real Banach space and $x\in E$ : $\int_0^1\big((n+1)t^n g(tx)+t^{n+1}Dg(tx)x\big)\,dt=g(x)$ .

Preamble

import Mathlib
import Definitions.Def_ContWeatherall_defs

open CategoryTheory ContinuousAlternatingMap
open scoped ContDiff

Formal statement

namespace ContWeatherall

/-- Radial fundamental theorem of calculus: `∫₀¹ d/dt (tⁿ⁺¹ g(t x)) dt = g x`, written out. -/
theorem integral_radial {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
    [CompleteSpace G] (n : ℕ) {g : E → G} (hg : ContDiff ℝ 1 g) (x : E) :
    ∫ t in (0 : ℝ)..1, (((n + 1 : ℕ) : ℝ) * t ^ n) • g (t • x) + t ^ (n + 1) • fderiv ℝ g (t • x) x
      = g x := by
  sorry

end ContWeatherall

Source

M. Spivak, Calculus on Manifolds (W. A. Benjamin, 1965), Theorem 4-11 (Poincaré lemma) and its proof (final integration step)

Read-back

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

Let $E,G$ be real normed spaces with $G$ complete, $n\in\mathbb{N}$ , $g:E\to G$ of class $C^1$ , and $x\in E$ . Then

\int_0^1\Big((n+1)\,t^{n}\;g(tx)+t^{n+1}\,Dg(tx)\,x\Big)\,dt=g(x),

an interval integral over $t\in[0,1]$ of a $G$ -valued function, where $Dg(tx)x$ is the Fréchet derivative of $g$ at $tx$ applied to $x$ .

View graph