Second Fréchet Derivative Along a Line

Proved

FunctionalInequalities.Analysis.CoordinateTensor.fderiv_fderiv_apply_eq_deriv_deriv_line_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement identifies a second Fréchet derivative evaluated twice in one direction with a one-dimensional second derivative.

Let $W$ be a real normed space, let $\Phi:W\to\mathbb R$ , and let $y\in W$ . Assume $\Phi$ is $C^2$ at $y$ . For every $v\in W$ ,

\bigl(D(D\Phi)(y)v\bigr)v =\left.\frac{d^2}{d\varepsilon^2}\Phi(y+\varepsilon v)\right|_{\varepsilon=0}.

This general calculus identity is used to convert second directional derivatives into derivatives along scalar lines.

Original Lean declaration header

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

theorem fderiv_fderiv_apply_eq_deriv_deriv_line {W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    {Φ : W → ℝ} {y : W} (hΦ : ContDiffAt ℝ 2 Φ y) (v : W) :
    fderiv ℝ (fderiv ℝ Φ) y v v = deriv (deriv fun ε : ℝ => Φ (y + ε • v)) 0

Module navigation

Module: Analysis/Tensor/EnergyForm.

Previous: sum_mul_prod_delta_erase_erase · Next: slot_sum_two.

Source excerpt, lines 613–615 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_EnergyForm

set_option maxHeartbeats 800000

Formal statement


theorem FunctionalInequalities.Analysis.CoordinateTensor.fderiv_fderiv_apply_eq_deriv_deriv_line_readable {W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    {Φ : W → ℝ} {y : W} (hΦ : ContDiffAt ℝ 2 Φ y) (v : W) :
    fderiv ℝ (fderiv ℝ Φ) y v v = deriv (deriv fun ε : ℝ => Φ (y + ε • v)) 0 := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Tensor/EnergyForm.lean#L611-L644 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Tensor.EnergyForm`, declaration `FunctionalInequalities.Analysis.CoordinateTensor.fderiv_fderiv_apply_eq_deriv_deriv_line`; the repository is private at upload time).

View graph