Differentiating the variation of an observable

Proved

BianchiIX.hasDerivAt_observable_variation

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

bianchi-ix-era-statisticsdynamical-systems

Let $E,F$ be real normed spaces, $p:E\to F$ , $f:E\to E$ , and $\alpha,v:\mathbb R\to E$ . Fix $t\in\mathbb R$ . Assume $p$ is $C^2$ and $f$ is differentiable at $\alpha(t)$ , with

\alpha'(t)=f(\alpha(t)),\qquad v'(t)=df_{\alpha(t)}v(t).

Then

\left.\frac{d}{ds}\bigl(dp_{\alpha(s)}v(s)\bigr)\right|_{s=t} =d\bigl[x\mapsto dp_xf(x)\bigr]_{\alpha(t)}v(t).

Preamble

import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Analysis.Calculus.Deriv.Mul
import Mathlib.Tactic.NormNum
import Mathlib.Analysis.Calculus.Deriv.Prod
import Mathlib.Tactic.Module

namespace BianchiIX
end BianchiIX

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

Formal statement

theorem BianchiIX.hasDerivAt_observable_variation
    {p : E → F} {f : E → E} {alpha v : ℝ → E} {t : ℝ}
    (hp : ContDiffAt ℝ 2 p (alpha t)) (hf : DifferentiableAt ℝ f (alpha t))
    (ha : HasDerivAt alpha (f (alpha t)) t)
    (hv : HasDerivAt v (fderiv ℝ f (alpha t) (v t)) t) :
    HasDerivAt (fun s => fderiv ℝ p (alpha s) (v s))
      (fderiv ℝ (fun x => fderiv ℝ p x (f x)) (alpha t) (v t)) t := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/ClockVariation.lean#L15-L33

View graph