Second Derivative of the Energy Form Along a Line

Proved

FunctionalInequalities.Analysis.CoordinateTensor.deriv_deriv_energyForm_line_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement formalizes the second-order energy-form identity associated with (88) of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $n,r\in\mathbb N$ , let $T,X$ be order- $r$ coordinate tensors on $\mathbb R^n$ , and let $H$ be a self-adjoint continuous linear operator on $\mathbb R^n$ . Writing $M$ for its standard matrix, define

F(\varepsilon)=\operatorname{energyForm}(I+\varepsilon H,T+\varepsilon X).

Then

F''(0)=2\left( \|X\|^2-2\langle X,\Sigma_M T\rangle +\frac12\|\Sigma_M T\|^2 +\frac12\sum_s\|M^{(s)}T\|^2 \right).

This is the exact second derivative along the specified line and is used in the tensor energy estimates.

Formalization Note The tensor inner product and norms are the finite coordinate sums defined in Lean; no dimension restriction beyond $n,r\in\mathbb N$ is imposed.

Original Lean declaration header

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

theorem deriv_deriv_energyForm_line (T : (Fin r → Fin n) → ℝ)
    (H : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) (hH : IsSelfAdjoint H)
    (X : (Fin r → Fin n) → ℝ) :
    deriv (deriv fun ε : ℝ => energyForm (1 + ε • H) (T + ε • X)) 0 =
      2 * (inner X X - 2 * inner X (actSum (stdMatrix H) T)
        + (1 / 2 : ℝ) * inner (actSum (stdMatrix H) T) (actSum (stdMatrix H) T)
        + (1 / 2 : ℝ) * ∑ s, inner (actOn (stdMatrix H) s T) (actOn (stdMatrix H) s T))

Module navigation

Module: Analysis/Tensor/EnergyForm.

Definition modules: Analysis/Tensor/SlotAction.

Supporting theorems: actOn_mul, inner_actOn_left, inner_actSum_actSum, slot_sum_two, two_slot_sum.

Previous: two_slot_sum.

Source excerpt, lines 883–889 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_EnergyForm

variable {n r : ℕ}
set_option maxHeartbeats 1600000

Formal statement


theorem FunctionalInequalities.Analysis.CoordinateTensor.deriv_deriv_energyForm_line_readable (T : (Fin r → Fin n) → ℝ)
    (H : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) (hH : IsSelfAdjoint H)
    (X : (Fin r → Fin n) → ℝ) :
    deriv (deriv fun ε : ℝ => energyForm (1 + ε • H) (T + ε • X)) 0 =
      2 * (inner X X - 2 * inner X (actSum (stdMatrix H) T)
        + (1 / 2 : ℝ) * inner (actSum (stdMatrix H) T) (actSum (stdMatrix H) T)
        + (1 / 2 : ℝ) * ∑ s, inner (actOn (stdMatrix H) s T) (actOn (stdMatrix H) s T)) := by sorry

Source

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

View graph