Directional derivatives along an ordered list
DefinitionKLSModular_FunctionalInequalities_Analysis_IteratedDerivative_Symmetryfunctional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context
directional hs f recursively applies Fréchet derivatives of a map in the inherited order of the list hs: the empty list returns , while prepending differentiates the result for the tail in direction . The definition assumes only real normed-space structures on and ; the module documentation records related symmetry results, but this bundle provides the definition itself.
Original module imports
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Data.List.FinRange
Original declaration excerpt
Shown in the original module context.
def directional : List E → (E → F) → E → F
| [], f => f
| h :: hs, f => fun x => fderiv ℝ (directional hs f) x h
Module navigation
Project result: The KLS conjecture.
Original module · FunctionalInequalities.Analysis.IteratedDerivative.Symmetry · Frozen source 408915f.
Definition code
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Data.List.FinRange
noncomputable section
open scoped ContDiff
namespace FunctionalInequalities
namespace Analysis
variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[NormedAddCommGroup F] [NormedSpace ℝ F]
/-- Successive directional derivatives in the inherited list order. -/
def directional : List E → (E → F) → E → F
| [], f => f
| h :: hs, f => fun x => fderiv ℝ (directional hs f) x h
end Analysis
end FunctionalInequalities
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/IteratedDerivative/Symmetry.lean#L24-L27 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.IteratedDerivative.Symmetry`, definition bundle `KLSModular_FunctionalInequalities_Analysis_IteratedDerivative_Symmetry`; the repository is private at upload time).