Affine Source Stein Identity

Proved

FunctionalInequalities.KLS.LogConcave.source_affine_stein_identity_of_bounded_lipschitz_test_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement gives the affine version of the source Stein identity.

Let $n\in\mathbb N$ . Let $u,h:\mathbb R^n\to\mathbb R$ be $C^1$ , with $u$ and $∇u$ globally Lipschitz and $\int e^{-u}=1$ . Let $h$ be globally Lipschitz and bounded by $C$ . For a continuous linear map $S$ , and vectors $z,v\in\mathbb R^n$ , both functions below are integrable under $ν=\operatorname{volume}.\operatorname{tilted}(-u)$ , and

\int \langle S∇u(y),v\rangle h(S∇u(y)+z)\,dν(y) = \int \left\langle S^*v,\operatorname{action}\!\left(\nabla^2u(y),S^*∇h(S∇u(y)+z)\right)\right\rangle dν(y).

This identity is the affine source component used in the Gaussian product coupling.

Original Lean declaration header

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

set_option maxHeartbeats 600000 in
theorem source_affine_stein_identity_of_bounded_lipschitz_test {n : ℕ}
    {u h : EuclideanSpace ℝ (Fin n) → ℝ} {L G Lh : NNReal}
    (hu : ContDiff ℝ 1 u) (hL : LipschitzWith L u)
    (hG : LipschitzWith G (gradient u))
    (hnorm : (∫ y, Real.exp (-u y) ∂volume) = 1)
    (hh : ContDiff ℝ 1 h) (hhLip : LipschitzWith Lh h)
    (C : ℝ) (hbound : ∀ x, ‖h x‖ ≤ C)
    (S : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n))
    (z v : EuclideanSpace ℝ (Fin n)) :
    Integrable (fun y => ⟪S (gradient u y), v⟫ * h (S (gradient u y) + z))
      ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u)) ∧
    Integrable (fun y => ⟪S.adjoint v,
      action (hessianMatrix u y) (S.adjoint (gradient h (S (gradient u y) + z)))⟫)
      ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u)) ∧
    (∫ y, ⟪S (gradient u y), v⟫ * h (S (gradient u y) + z)
      ∂((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u))) =
      ∫ y, ⟪S.adjoint v,
        action (hessianMatrix u y) (S.adjoint (gradient h (S (gradient u y) + z)))⟫
        ∂((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u))

Module navigation

Module: KLS/LogConcave/HessianStein.

Definition modules: Analysis/BakryEmery/HessianOperator, Probability/Stein/Kernel.

Supporting theorems: source_stein_identity_of_bounded_lipschitz_test.

Previous: source_stein_identity_of_bounded_lipschitz_test.

Source excerpt, lines 352–371 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HessianStein

open MeasureTheory
open FunctionalInequalities.Probability.Stein
open scoped ContDiff RealInnerProductSpace
set_option maxHeartbeats 600000

Formal statement

theorem FunctionalInequalities.KLS.LogConcave.source_affine_stein_identity_of_bounded_lipschitz_test_readable {n : ℕ}
    {u h : EuclideanSpace ℝ (Fin n) → ℝ} {L G Lh : NNReal}
    (hu : ContDiff ℝ 1 u) (hL : LipschitzWith L u)
    (hG : LipschitzWith G (gradient u))
    (hnorm : (∫ y, Real.exp (-u y) ∂volume) = 1)
    (hh : ContDiff ℝ 1 h) (hhLip : LipschitzWith Lh h)
    (C : ℝ) (hbound : ∀ x, ‖h x‖ ≤ C)
    (S : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n))
    (z v : EuclideanSpace ℝ (Fin n)) :
    Integrable (fun y => ⟪S (gradient u y), v⟫ * h (S (gradient u y) + z))
      ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u)) ∧
    Integrable (fun y => ⟪S.adjoint v,
      action (hessianMatrix u y) (S.adjoint (gradient h (S (gradient u y) + z)))⟫)
      ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u)) ∧
    (∫ y, ⟪S (gradient u y), v⟫ * h (S (gradient u y) + z)
      ∂((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u))) =
      ∫ y, ⟪S.adjoint v,
        action (hessianMatrix u y) (S.adjoint (gradient h (S (gradient u y) + z)))⟫
        ∂((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u)) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/HessianStein.lean#L352-L385 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.HessianStein`, declaration `FunctionalInequalities.KLS.LogConcave.source_affine_stein_identity_of_bounded_lipschitz_test`; the repository is private at upload time).

View graph