Prove2Me

ContDiff of a parameter-dependent interval integral on [0,1][0,1]

Proved
NewtonCartan.contDiff_integral_I01

by Ethan Cheung Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysiscont-diffnewton-cartan

Let EE be a finite-dimensional real normed space. If a function g:E×R→Rg : E \times \mathbb{R} \to \mathbb{R} is of class CnC^n (for n∈N∪{∞}n \in \mathbb{N}\cup\{\infty\}), then the parameter-dependent integral

x↦∫01g(x,s) dsx \mapsto \int_0^1 g(x,s)\,ds

is likewise of class CnC^n as a map E→RE \to \mathbb{R}.

This is the standard differentiation-under-the-integral statement for continuous dependence of the integrand on the parameter, specialized to the compact interval [0,1][0,1] and used as a building block for ContDiff assembly of radial Poincaré potentials.

Preamble
import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.Analysis.Calculus.ContDiff.Operations
import Mathlib.Analysis.Calculus.ContDiff.Comp
import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
import Mathlib.Analysis.Calculus.ParametricIntervalIntegral
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
import Mathlib.MeasureTheory.Integral.DominatedConvergence
import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
import Mathlib.Topology.MetricSpace.Basic
import Mathlib.Analysis.Normed.Operator.Basic

open scoped ContDiff Topology Interval
open MeasureTheory Metric Set Filter ContinuousLinearMap
Formal statement
namespace NewtonCartan

theorem contDiff_integral_I01 {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [CompleteSpace E] [FiniteDimensional ℝ E]
    (n : ℕ∞) (g : E → ℝ → ℝ)
    (hg : ContDiff ℝ n (fun p : E × ℝ => g p.1 p.2)) :
    ContDiff ℝ n (fun x : E => ∫ s in (0 : ℝ)..1, g x s) := by sorry

end NewtonCartan
Source
Standard fact from multivariable calculus / Mathlib ParametricIntervalIntegral; needed for Trautman recovery (Newton–Cartan Prop. 2.2) spatial potential assembly

View graph