Gradient Jets Pair With the Next Derivative

This is a calculus identity relating iterated derivatives of a gradient to the next iterated derivative of the original function.

Let $E$ be a complete real inner-product space, and let $f : E \to \mathbb{R}$ be infinitely differentiable, expressed by the hypothesis ContDiff ℝ ∞ f. For every natural number $r$, point $x \in E$, direction family $h : \operatorname{Fin}(r) \to E$, and additional direction $w \in E$, the inner product of the $r$-th iterated derivative of the gradient with $w$ equals the $(r+1)$-st iterated derivative of $f$, evaluated on the directions in $h$ followed by $w$:

Here gradient denotes the gradient of $f$, iteratedFDeriv denotes the iterated Fréchet derivative, and Fin.snoc h w appends $w$ as the final direction to the family $h$.

This is a reusable identity for converting gradient-jet expressions into higher derivatives of a scalar-valued function, with no restriction on the order $r$ or the dimension of $E$.

Formalization Note The derivatives are real Fréchet derivatives, the inner product is the real inner product on the complete space $E$, and the equality is pointwise for every choice of $r$, $x$, $h$, and $w$.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem inner_iteratedFDeriv_gradient_apply {f : E → ℝ} (hf : ContDiff ℝ ∞ f) (r : ℕ) (x : E)
    (h : Fin r → E) (w : E) :
    ⟪iteratedFDeriv ℝ r (gradient f) x h, w⟫ = iteratedFDeriv ℝ (r + 1) f x (Fin.snoc h w)

Module navigation

Module: Analysis/IteratedDerivative/GradientJet.

Previous: iteratedFDeriv_sub_const_of_pos.

Source excerpt, lines 55–57 · Frozen source 408915f.