Additivity of the Centered Gradient

Proved

FunctionalInequalities.KLS.LogConcave.PoissonIterate.grad0_sub_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

Let $T$ be a linear gradient-type partial operator, and let $u,v$ be level- $k$ fields whose components all lie in the domain of $T$ . Then the centered gradient is additive:

\nabla_0(u-v)=\nabla_0u-\nabla_0v.

The equality is componentwise as a field of $L^2(\nu;V)$ classes. This is a technical linearity lemma used when comparing Poisson steps under permutations.

Original Lean declaration header

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

theorem grad0_sub {k : ℕ} {u v : Field ν k} (hu : ∀ I, u I ∈ T.domain)
    (hv : ∀ I, v I ∈ T.domain) : grad0 T (u - v) = grad0 T u - grad0 T v

Module navigation

Module: KLS/BKL/PoissonIterate/Symmetry.

Definition modules: KLS/BKL/PoissonIterate/Basic.

Next: grad0_step_sub_permField_succ.

Source excerpt, lines 122–123 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Symmetry

variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] {ν : MeasureTheory.ProbabilityMeasure V}
  (T : MeasureTheory.Lp ℝ 2 (ν : MeasureTheory.Measure V) →ₗ.[ℝ] MeasureTheory.Lp V 2 (ν : MeasureTheory.Measure V))

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.PoissonIterate.grad0_sub_readable {k : ℕ} {u v : Field ν k} (hu : ∀ I, u I ∈ T.domain)
    (hv : ∀ I, v I ∈ T.domain) : grad0 T (u - v) = grad0 T u - grad0 T v := by sorry

Source

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

View graph