Coordinate Taylor Tensor Generator Identity

This formalizes BKL Lemma 3.6 in coordinates.

Let $V$ be finite-dimensional, let $\nu=m\mathbin{.}\mathrm{tilted}(-U)$ with $U\in C^2$, and assume all exponential moments of $\nu$ are integrable. Let $u$ lie in the domain of $A=\bar T^\dagger\bar T$. For $d\in\mathbb N$ and an index map $i:\mathrm{Fin}(d+1)\to\mathrm{Fin}(\dim V)$, write $e_j$ for the standard orthonormal basis. Then the $(d+1)$st Taylor tensor of $Au$ satisfies

The sum averages over all permutations of the $d+1$ coordinate positions.

This coordinate identity is the tensor form of the generator–gradient tilt identity and is reused in the Poisson-iterate Taylor estimates.

Formalization Note: Taylor tensors are formed from $L^2(\nu)$ representatives, and the coordinate indices use Fin (Module.finrank ℝ V).

Original Lean declaration header

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

theorem taylorTensor_gen_apply {u : Lp ℝ 2 (ν : Measure V)} (hu : u ∈ (adjointComp T̄).domain)
    (d : ℕ) (i : Fin (d + 1) → Fin (Module.finrank ℝ V)) :
    taylorTensor (ν : Measure V) (⇑(gen T̄ u)) (d + 1) (fun p => stdOrthonormalBasis ℝ V (i p)) =
      ((d + 1).factorial : ℝ)⁻¹ * ∑ τ : Equiv.Perm (Fin (d + 1)),
        taylorTensor (ν : Measure V) (⇑(partialDeriv T̄ (i (τ (Fin.last d))) u)) d
          (fun p => stdOrthonormalBasis ℝ V (i (τ (Fin.castSucc p))))

Module navigation

Module: KLS/BKL/PoissonIterate/Taylor.

Definition modules: KLS/BKL/PoissonIterate/Basic, KLS/LogConcave/WeightedGradient/Closure, Analysis/Semigroup/AdjointComp, Probability/LogConcave, Analysis/BakryEmery/Tilt/Basic.

Supporting theorems: contDiff_tiltAverage_of_memLp, integrable_expTilt_of_memLp, taylorTensor_succ_of_eq_inner, tiltAverage_adjointComp_eq.

Previous: symmetrize_apply_comp_cast · Next: symmetrize_taylorField_grad0_step.

Source excerpt, lines 254–259 · Frozen source 408915f.