Higher Derivative Invariance Under Constant Shifts

Proved

FunctionalInequalities.Analysis.iteratedFDeriv_sub_const_of_pos_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the shift invariance of positive-order iterated derivatives.

Let $E$ and $F$ be real normed spaces, let $f:E\to F$ be smooth, let $c\in F$ , let $r\in\mathbb N$ satisfy $r\geq1$ , and let $x\in E$ . Then

D^r(f-c)(x)=D^rf(x).

Here $f-c$ denotes the function $z\mapsto f(z)-c$ . The conclusion is stated using iteratedFDeriv; no inner-product, completeness, finite-dimensionality, or measure assumptions are required.

Original Lean declaration header

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

theorem iteratedFDeriv_sub_const_of_pos {f : E → F} (hf : ContDiff ℝ ∞ f) (c : F) {r : ℕ} (hr : 1 ≤ r)
    (x : E) : iteratedFDeriv ℝ r (fun z => f z - c) x = iteratedFDeriv ℝ r f x

Module navigation

Module: Analysis/IteratedDerivative/GradientJet.

Next: inner_iteratedFDeriv_gradient_apply.

Source excerpt, lines 31–32 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_IteratedDerivative_GradientJet

open scoped RealInnerProductSpace ContDiff
variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F]

Formal statement


theorem FunctionalInequalities.Analysis.iteratedFDeriv_sub_const_of_pos_readable {f : E → F} (hf : ContDiff ℝ ∞ f) (c : F) {r : ℕ} (hr : 1 ≤ r)
    (x : E) : iteratedFDeriv ℝ r (fun z => f z - c) x = iteratedFDeriv ℝ r f x := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/IteratedDerivative/GradientJet.lean#L29-L45 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.IteratedDerivative.GradientJet`, declaration `FunctionalInequalities.Analysis.iteratedFDeriv_sub_const_of_pos`; the repository is private at upload time).

View graph