Taylor Tensors Ignore Centering

Proved

FunctionalInequalities.KLS.LogConcave.PoissonIterate.taylorTensor_center_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

Let $\nu$ be a probability measure on a finite-dimensional Borel space with all exponential moments, let $u\in L^2(\nu)$ , and let $d\ge1$ . Then the degree- $d$ Taylor tensor is unchanged by centering:

T_d\left(u-\int u\,d\nu\right)=T_d(u).

Equivalently, using the formalization's L2.center,

T_d(\operatorname{center}(u))=T_d(u).

This is a technical fact used to replace weak derivatives by their centered versions in Taylor-tensor identities. No finite-dimensional assumption is required by this declaration beyond the Borel structure shown in the type.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.LogConcave.PoissonIterate. Shown in its original module context. Proof omitted.

theorem taylorTensor_center
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) (ν : Measure V))
    (u : Lp ℝ 2 (ν : Measure V)) {d : ℕ} (hd : 1 ≤ d) :
    taylorTensor (ν : Measure V) (⇑(L2.center ν u)) d = taylorTensor (ν : Measure V) (⇑u) d

Module navigation

Module: KLS/BKL/PoissonIterate/Taylor.

Definition modules: Analysis/BakryEmery/Tilt/Basic, L2/MeanVariance.

Supporting theorems: integrable_expTilt_of_memLp.

Next: symmetrize_apply_comp_cast.

Source excerpt, lines 96–99 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Taylor

open MeasureTheory
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {ν : MeasureTheory.ProbabilityMeasure V}
omit [FiniteDimensional ℝ V]

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.PoissonIterate.taylorTensor_center_readable
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) (ν : Measure V))
    (u : Lp ℝ 2 (ν : Measure V)) {d : ℕ} (hd : 1 ≤ d) :
    taylorTensor (ν : Measure V) (⇑(L2.center ν u)) d = taylorTensor (ν : Measure V) (⇑u) d := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/PoissonIterate/Taylor.lean#L94-L110 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.PoissonIterate.Taylor`, declaration `FunctionalInequalities.KLS.LogConcave.PoissonIterate.taylorTensor_center`; the repository is private at upload time).

View graph