One-Step Taylor-Field Symmetrization Identity

Proved

FunctionalInequalities.KLS.LogConcave.PoissonIterate.symmetrize_taylorField_grad0_step_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes BKL Corollary 3.7 for one step.

Let $V$ be finite-dimensional, let $\nu=m\mathbin{.}\mathrm{tilted}(-U)$ with $U\in C^2$ and all exponential moments, and assume $C_P(\nu)\le C$ . Let $h$ be a level- $k$ field and let $d\ge1$ . For every coefficient index array $J$ of length $d+1+k+1$ , the symmetrization over the first $d+1$ Taylor positions of the degree- $d$ Taylor field of the centered gradient of the Poisson step equals the scale times the degree- $(d+1)$ Taylor field of the centered gradient of $h$ :

S_{d+1}T_d\bigl(\nabla_0(\operatorname{step}(h))\bigr) =\operatorname{scale}(h)\,T_{d+1}(\nabla_0h).

The two coefficient arrays are identified through the finite-index cast specified in the formal statement.

This identity is the one-step relation iterated in the Taylor recursion.

Original Lean declaration header

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

theorem symmetrize_taylorField_grad0_step {k : ℕ} (h : Field ν k) {d : ℕ} (hd : 1 ≤ d)
    (J : Fin (d + 1 + (k + 1)) → Fin (Module.finrank ℝ V)) :
    symmetrize (Module.finrank ℝ V) (d + (k + 2)) (d + 1)
        (taylorField d (grad0 T̄ (step T̄ h))) (J ∘ Fin.cast (by omega)) =
      scale T̄ h * taylorField (d + 1) (grad0 T̄ h) J

Module navigation

Module: KLS/BKL/PoissonIterate/Taylor.

Definition modules: KLS/LogConcave/WeightedGradient/Closure, KLS/BKL/PoissonIterate/Basic, Probability/LogConcave, Analysis/Tensor/Coordinate, Poincare/LocalSlope/Basic.

Supporting theorems: taylorTensor_const_mul, symmetrize_apply_comp_cast, taylorTensor_center, taylorTensor_gen_apply, existsUnique_centered_adjointComp_eq.

Previous: taylorTensor_gen_apply · Next: meanGradSq_eq_norm_taylorField_one_genField.

Source excerpt, lines 278–282 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Taylor

open FunctionalInequalities.Analysis.Tensor
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
  {ν : MeasureTheory.ProbabilityMeasure V} (m : MeasureTheory.Measure V) [m.IsAddHaarMeasure] (hν : FunctionalInequalities.KLS.LogConcave ν)
  (hi : (interior (ν : MeasureTheory.Measure V).support).Nonempty) {U : V → ℝ}
  (hνU : (ν : MeasureTheory.Measure V) = m.tilted (-U)) (hU : ContDiff ℝ 2 U)
  (hexp : ∀ r : ℝ, MeasureTheory.Integrable (fun x => Real.exp (r * ‖x‖)) (ν : MeasureTheory.Measure V))
local notation "T̄" => hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
variable {C : NNReal} (hC : FunctionalInequalities.Poincare.LocalSlope.Intrinsic.constant ν ≤ (C : ENNReal))
include hνU hU hexp hC

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.PoissonIterate.symmetrize_taylorField_grad0_step_readable {k : ℕ} (h : Field ν k) {d : ℕ} (hd : 1 ≤ d)
    (J : Fin (d + 1 + (k + 1)) → Fin (Module.finrank ℝ V)) :
    symmetrize (Module.finrank ℝ V) (d + (k + 2)) (d + 1)
        (taylorField d (grad0 T̄ (step T̄ h))) (J ∘ Fin.cast (by omega)) =
      scale T̄ h * taylorField (d + 1) (grad0 T̄ h) J := by sorry

Source

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

View graph