Successor Taylor Tensor from an Inner-Product Identity

This statement formalizes the tensor identity corresponding to Lemma 3.6 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $E$ be a real inner-product space that is complete and measurable, let $\mu$ be a measure on $E$, and let $g:E\to\mathbb R$ and $G:E\to E$. Assume:

1. The tilt average $F_G=\operatorname{tiltAverage}(\mu,G)$ is infinitely continuously differentiable.
2. The tilt average of $g$ satisfies, for every $w\in E$,

$$F_g(w)=\langle w,F_G(w)\rangle.$$

3. $d\in\mathbb N$.

Then

$$T_{d+1}g=\operatorname{symmetrizeML}\bigl(\operatorname{appendInner}(T_dG)\bigr).$$

The result isolates the tensor consequence of the tilt identity and can be reused independently of compact-support assumptions used elsewhere.

Formalization Note The statement has no finite-dimensionality or Borel-space hypothesis. The definitions tiltAverage, taylorTensor, appendInner, and symmetrizeML are used exactly as Lean defines them.

Original Lean declaration header

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

theorem taylorTensor_succ_of_eq_inner (μ : Measure E) {g : E → ℝ} {G : E → E}
    (hG : ContDiff ℝ ∞ (tiltAverage μ G))
    (hEq : tiltAverage μ g = fun w => ⟪w, tiltAverage μ G w⟫) (d : ℕ) :
    taylorTensor μ g (d + 1) = symmetrizeML (appendInner (taylorTensor μ G d))

Module navigation

Module: Analysis/BakryEmery/Tilt/SquareIntegrable.

Definition modules: Analysis/Tensor/Multilinear, Analysis/BakryEmery/Tilt/Basic.

Supporting theorems: iteratedFDeriv_comp_perm_of_contDiff, iteratedFDeriv_inner_self_apply, sum_perm_inner_init_last.

Previous: integrable_expTilt_of_memLp.

Source excerpt, lines 695–698 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Tilt_SquareIntegrable

open MeasureTheory Filter Topology FunctionalInequalities.Analysis.Tensor
open scoped RealInnerProductSpace ContDiff ENNReal
universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
omit [FiniteDimensional ℝ E] [BorelSpace E]

theorem FunctionalInequalities.Analysis.BakryEmery.taylorTensor_succ_of_eq_inner_readable (μ : Measure E) {g : E → ℝ} {G : E → E}
    (hG : ContDiff ℝ ∞ (tiltAverage μ G))
    (hEq : tiltAverage μ g = fun w => ⟪w, tiltAverage μ G w⟫) (d : ℕ) :
    taylorTensor μ g (d + 1) = symmetrizeML (appendInner (taylorTensor μ G d)) := by sorry