Prove2Me

Coordinate Tensor Bound in an Arbitrary Orthonormal Basis

Proved
FunctionalInequalities.Analysis.BakryEmery.norm_coordTensor_taylorTensor_inner_sq_le_of_basis_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the linear-function step cited on page 30 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), Proposition 7.1.

Let μ\mu be a probability measure on a finite-dimensional real inner-product space EE with all exponential moments. Let bEb_E be an orthonormal basis indexed by Fin⁡(m)\operatorname{Fin}(m). Fix d∈Nd\in\mathbb N, b∈Rb\in\mathbb R, and assume that for every u∈Eu\in E,

∑J:Fin⁡(d)→Fin⁡(m)κd+1(u,bE∘J)2≤b∥u∥2.\sum_{J:\operatorname{Fin}(d)\to\operatorname{Fin}(m)}\kappa_{d+1}(u,b_E\circ J)^2\le b\|u\|^2.

Then for every v∈Ev\in E,

∥coordTensor⁡bE ⁣(Td(x↦⟨v,x⟩))∥2≤b(d!)2∥v∥2.\left\|\operatorname{coordTensor}_{b_E}\!\left(T_d(x\mapsto\langle v,x\rangle)\right)\right\|^2 \le \frac{b}{(d!)^2}\|v\|^2.

The result transfers a cumulant contraction estimate to the coordinate tensor of the Taylor tensor in any orthonormal basis.

Original Lean declaration header

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

theorem norm_coordTensor_taylorTensor_inner_sq_le_of_basis (μ : Measure E) [IsProbabilityMeasure μ]
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) μ) {m : ℕ}
    (bE : OrthonormalBasis (Fin m) ℝ E) {d : ℕ} {b : ℝ}
    (hR : ∀ u : E, ∑ J : Fin d → Fin m,
      cumulant μ (d + 1) (Fin.cons u fun k => bE (J k)) ^ 2 ≤ b * ‖u‖ ^ 2) (v : E) :
    ‖Analysis.Tensor.coordTensor bE (taylorTensor μ (fun x => ⟪v, x⟫) d)‖ ^ 2 ≤
      b / (d.factorial : ℝ) ^ 2 * ‖v‖ ^ 2

Module navigation

Module: Analysis/BakryEmery/Cumulant/Basic.

Definition modules: Analysis/Tensor/Coefficients, Analysis/Tensor/Coordinate, Analysis/BakryEmery/Tilt/Basic.

Supporting theorems: taylorTensor_inner_eq_cumulant.

Previous: taylorTensor_inner_eq_cumulant · Next: contDiffOn_logLaplace_ball.

Source excerpt, lines 721–727 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Cumulant_Basic

open MeasureTheory
open scoped RealInnerProductSpace ContDiff
universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
omit [CompleteSpace E]
Formal statement

theorem FunctionalInequalities.Analysis.BakryEmery.norm_coordTensor_taylorTensor_inner_sq_le_of_basis_readable (μ : Measure E) [IsProbabilityMeasure μ]
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) μ) {m : ℕ}
    (bE : OrthonormalBasis (Fin m) ℝ E) {d : ℕ} {b : ℝ}
    (hR : ∀ u : E, ∑ J : Fin d → Fin m,
      cumulant μ (d + 1) (Fin.cons u fun k => bE (J k)) ^ 2 ≤ b * ‖u‖ ^ 2) (v : E) :
    ‖Analysis.Tensor.coordTensor bE (taylorTensor μ (fun x => ⟪v, x⟫) d)‖ ^ 2 ≤
      b / (d.factorial : ℝ) ^ 2 * ‖v‖ ^ 2 := by sorry
Source
Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Proposition 7.1, p. 28. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Cumulant/Basic.lean#L718-L755 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Cumulant.Basic`, declaration `FunctionalInequalities.Analysis.BakryEmery.norm_coordTensor_taylorTensor_inner_sq_le_of_basis`; the repository is private at upload time).

View graph