The derivative of a parameter integral with a moving endpoint

Proved

BianchiIX.hasFDerivAt_moving_intervalIntegral_of_contDiffAt

by trppppp · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

bianchi-ix-era-statisticsdynamical-systems

Let $E$ be a real normed space, $F:E\times\mathbb R\to\mathbb R$ , $\tau:E\to\mathbb R$ , and $x\in E$ . Assume $\tau(x)\geq0$ and define

M_F(y)=\int_0^{\tau(y)}F(y,t)\,dt,\qquad R(y,s)=\tau(y)F(y,s\tau(y)).

All interval integrals are oriented integrals. Suppose $\tau$ is $C^1$ at $x$ and $F$ is $C^1$ at $(x,t)$ for every $t\in[0,\tau(x)]$ . Then $M_F$ is Frechet differentiable at $x$ , with

d(M_F)_x=\int_0^1 dR_{(x,s)}\circ\iota_E\,ds,\qquad \iota_E(v)=(v,0).

Preamble

import Mathlib.Analysis.Calculus.ParametricIntervalIntegral
import Mathlib.Analysis.Calculus.ContDiff.Operations
import Mathlib.Topology.Order.Compact

namespace BianchiIX
end BianchiIX

noncomputable section
open BianchiIX
open Set Filter MeasureTheory
open scoped Topology
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]

Formal statement

theorem BianchiIX.hasFDerivAt_moving_intervalIntegral_of_contDiffAt
    {F : E × ℝ → ℝ} {τ : E → ℝ} {x : E} (hτ : ContDiffAt ℝ 1 τ x) (hpos : 0 ≤ τ x)
    (hF : ∀ t ∈ Icc 0 (τ x), ContDiffAt ℝ 1 F (x, t)) :
    HasFDerivAt (fun y => ∫ t in 0..τ y, F (y, t))
      (∫ t in (0 : ℝ)..1,
        (fderiv ℝ (fun p : E × ℝ => τ p.1 * F (p.1, p.2 * τ p.1)) (x, t)).comp
          (ContinuousLinearMap.inl ℝ E ℝ)) x := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/CompactParametricIntegral.lean#L61-L82

View graph