One-Step Hessian Defect Decomposition

Proved

FunctionalInequalities.KLS.LogConcave.PoissonIterate.normSq_gradField_gradField_step_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes BKL (47) for one Poisson step.

Let $V$ be finite-dimensional, let $\nu=m\mathbin{.}\mathrm{tilted}(-U)$ with $U$ of temperate growth and all exponential moments, and assume $C_P(\nu)\le C$ . Let $h$ be a field whose components lie in the domain of $A=\bar T^\dagger\bar T$ . Let $h'=\operatorname{step}(h)=\alpha(-L)^{-1}\nabla_0h$ , where $\alpha=\operatorname{scale}(h)$ . Then

\|\nabla^2h\|^2=\|Lh'\|^2+\|\nabla^2h-\alpha\nabla h'\|^2.

In the formalization, the final term is defect h, genField (step h) represents the generator field, and normSq is the squared Hilbert–Schmidt norm of the indexed field.

This Pythagorean identity is the basic one-step energy relation behind the defect estimates.

Original Lean declaration header

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

theorem normSq_gradField_gradField_step {k : ℕ} (h : Field ν k)
    (hh : ∀ I, h I ∈ (adjointComp T̄).domain) :
    normSq (gradField T̄ (gradField T̄ h)) = normSq (genField T̄ (step T̄ h)) + defect T̄ h

Module navigation

Module: KLS/BKL/PoissonIterate/Defect.

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

Selected supporting theorems: closedWeightedOperator_id_gap_of_literature_le, convexOn_of_eq_tilted, existsUnique_centered_adjointComp_eq, inner_center_center, sum_norm_sq_compLp_innerSL.

Next: gradField_gradField_comp_swap.

Source excerpt, lines 185–187 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Defect

open FunctionalInequalities.Analysis.Semigroup
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)) (hUt : U.HasTemperateGrowth)
  (hexp : ∀ r : ℝ, MeasureTheory.Integrable (fun x => Real.exp (r * ‖x‖)) (ν : MeasureTheory.Measure V))
  {C : NNReal} (hC : FunctionalInequalities.Poincare.LocalSlope.Intrinsic.constant ν ≤ (C : ENNReal))
local notation "T̄" => hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
include hνU hUt hexp hC

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.PoissonIterate.normSq_gradField_gradField_step_readable {k : ℕ} (h : Field ν k)
    (hh : ∀ I, h I ∈ (adjointComp T̄).domain) :
    normSq (gradField T̄ (gradField T̄ h)) = normSq (genField T̄ (step T̄ h)) + defect T̄ h := by sorry

Source

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

View graph