Prove2Me

Higher Leibniz Rule for an Inner Product Quadratic Form

Proved
FunctionalInequalities.Analysis.BakryEmery.iteratedFDeriv_inner_self_apply_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the higher-order Leibniz rule for the map w↦⟨w,G(w)⟩w\mapsto\langle w,G(w)\rangle.

Let EE be a real inner-product space, let G:E→EG:E\to E be C∞C^\infty, let d∈Nd\in\mathbb N, let z∈Ez\in E, and let h:Fin⁡(d+1)→Eh:\operatorname{Fin}(d+1)\to E. Then

Dd+1(w↦⟨w,G(w)⟩)(z)[h]=⟨z,Dd+1G(z)[h]⟩+∑k=0d⟨hk,DdG(z)[h with hk removed]⟩.D^{d+1}\bigl(w\mapsto\langle w,G(w)\rangle\bigr)(z)[h] =\left\langle z,D^{d+1}G(z)[h]\right\rangle +\sum_{k=0}^{d}\left\langle h_k,D^dG(z)[h\text{ with }h_k\text{ removed}]\right\rangle.

The formula is a reusable pointwise identity for differentiating quadratic forms whose first factor is the identity map.

Original Lean declaration header

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

theorem iteratedFDeriv_inner_self_apply {G : E → E} (hG : ContDiff ℝ ∞ G) (d : ℕ) (z : E)
    (h : Fin (d + 1) → E) :
    iteratedFDeriv ℝ (d + 1) (fun w => ⟪w, G w⟫) z h =
      ⟪z, iteratedFDeriv ℝ (d + 1) G z h⟫ +
        ∑ k : Fin (d + 1), ⟪h k, iteratedFDeriv ℝ d G z (k.removeNth h)⟫

Module navigation

Module: Analysis/BakryEmery/IteratedDerivative.

Next: iteratedFDeriv_succ_comp_perm_of_fix_zero.

Source excerpt, lines 45–49 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_IteratedDerivative

open scoped RealInnerProductSpace ContDiff
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
Formal statement

theorem FunctionalInequalities.Analysis.BakryEmery.iteratedFDeriv_inner_self_apply_readable {G : E → E} (hG : ContDiff ℝ ∞ G) (d : ℕ) (z : E)
    (h : Fin (d + 1) → E) :
    iteratedFDeriv ℝ (d + 1) (fun w => ⟪w, G w⟫) z h =
      ⟪z, iteratedFDeriv ℝ (d + 1) G z h⟫ +
        ∑ k : Fin (d + 1), ⟪h k, iteratedFDeriv ℝ d G z (k.removeNth h)⟫ := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/IteratedDerivative.lean#L43-L118 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.IteratedDerivative`, declaration `FunctionalInequalities.Analysis.BakryEmery.iteratedFDeriv_inner_self_apply`; the repository is private at upload time).

View graph