Gradient Second Moments Under an Isotropic Pushforward

Proved

FunctionalInequalities.KLS.integral_fderiv_mul_fderiv_eq_inner_of_isotropic_map_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This formalizes the second-moment identity in Lemma 2.3 of Letwin (arXiv:2607.24164v1).

Let $\nu$ be a probability measure on a finite-dimensional real inner-product space, let $\phi:E\to\mathbb{R}$ , and assume gradient φ is measurable. If the pushforward $(\nabla\phi)_*\nu$ is isotropic, then for every $u,v\in E$ ,

\int D\phi(x)[u]D\phi(x)[v]\,d\nu(x)=\langle u,v\rangle.

The conclusion uses the isotropy of the pushforward only; no convexity or regularity of $\phi$ beyond the stated measurable gradient representation is assumed.

Original Lean declaration header

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

theorem integral_fderiv_mul_fderiv_eq_inner_of_isotropic_map
    (ν : ProbabilityMeasure E) {φ : E → ℝ} (hφ : Measurable (gradient φ))
    (hiso : Isotropic (ν.map hφ.aemeasurable)) (u v : E) :
    ∫ x, fderiv ℝ φ x u * fderiv ℝ φ x v ∂(ν : Measure E) = ⟪u, v⟫

Module navigation

Module: KLS/Isotropic.

Previous: Isotropic.map_linearIsometryEquiv · Next: Isotropic.integral_norm_sq.

Source excerpt, lines 145–148 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_Isotropic

open MeasureTheory
open scoped RealInnerProductSpace
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
variable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

Formal statement


theorem FunctionalInequalities.KLS.integral_fderiv_mul_fderiv_eq_inner_of_isotropic_map_readable
    (ν : ProbabilityMeasure E) {φ : E → ℝ} (hφ : Measurable (gradient φ))
    (hiso : Isotropic (ν.map hφ.aemeasurable)) (u v : E) :
    ∫ x, fderiv ℝ φ x u * fderiv ℝ φ x v ∂(ν : Measure E) = ⟪u, v⟫ := by sorry

Source

Source: Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), Lemma 2.3. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/Isotropic.lean#L143-L173 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.Isotropic`, declaration `FunctionalInequalities.KLS.integral_fderiv_mul_fderiv_eq_inner_of_isotropic_map`; the repository is private at upload time).

View graph