Second Derivative Along a First-Factor Direction

This is a calculus identity for a function on a product space.

Let $E$ and $L$ be real normed spaces, with $E$ an inner-product space, and let $H:E\times L\to\mathbb R$ be twice continuously differentiable. For $p=(p_1,p_2)\in E\times L$ and $u\in E$, the second derivative of $H$ at $p$ in the product-space direction $(u,0)$, applied twice, equals the iterated second derivative of the restriction $y\mapsto H(y,p_2)$ in direction $u$:

The result is a technical partial-derivative identity, useful when expressing product-space Hessians through derivatives in the first parameter.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.BKL.Localization. Shown in its original module context. Proof omitted.

theorem fderiv_fderiv_fst_dir (H : E × L → ℝ) (hH : ContDiff ℝ 2 H) (p : E × L) (u : E) :
    fderiv ℝ (fderiv ℝ H) p (u, 0) (u, 0) =
      bilinearIteratedFDerivTwo ℝ (fun y => H (y, p.2)) p.1 u u

Module navigation

Module: KLS/BKL/Localization/LogLaplaceGenerator.

Next: sum_bilin_inverseSqrt_eq.

Source excerpt, lines 67–69 · Frozen source 408915f.