The chain rule for a scalar function evaluated at a moving endpoint

Proved

BianchiIX.fderiv_variable_endpoint

by trppppp · Nov 5, 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$ , and $\tau:E\to\mathbb R$ . Suppose $F$ is differentiable at $(x,\tau(x))$ and $\tau$ at $x$ . If the state slice $y\mapsto F(y,\tau(x))$ has Frechet derivative $A$ at $x$ , and the time slice $t\mapsto F(x,t)$ has derivative $b$ at $\tau(x)$ , then

d\bigl(y\mapsto F(y,\tau(y))\bigr)_xv=Av+b\,d\tau_xv.

Preamble

import Mathlib.Analysis.Calculus.ParametricIntervalIntegral
import Mathlib.Analysis.Calculus.ContDiff.Operations
import Mathlib.Topology.Order.Compact
import Mathlib.Analysis.Calculus.Deriv.Prod
import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
import Mathlib.Tactic.Ring

namespace BianchiIX
end BianchiIX

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

Formal statement

theorem BianchiIX.fderiv_variable_endpoint {F : E × ℝ → ℝ} {τ : E → ℝ} {x : E}
    {A : E →L[ℝ] ℝ} {b : ℝ} (hF : DifferentiableAt ℝ F (x, τ x))
    (hτ : DifferentiableAt ℝ τ x) (hleft : HasFDerivAt (fun y => F (y, τ x)) A x)
    (hright : HasDerivAt (fun t => F (x, t)) b (τ x)) (v : E) :
    fderiv ℝ (fun y => F (y, τ y)) x v = A v + b * fderiv ℝ τ x v := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/MovingIntegralDerivative.lean#L14-L32

View graph