Weak Source Stein Identity

This statement formalizes the weak source Stein identity associated with a normalized potential.

Let $n\in\mathbb N$. Let $u,f:\mathbb R^n\to\mathbb R$ be $C^1$, let $u$ and $∇u$ be globally Lipschitz, and assume

Let $f$ be globally Lipschitz and bounded by $C$. For every coordinate $i\in\operatorname{Fin}(n)$, both displayed integrands are integrable with respect to the tilted measure volume.tilted (-u), and

where $ν=\operatorname{volume}.\operatorname{tilted}(-u)$. This is an analytic identity; it does not assert existence of an inverse gradient map or a target Stein kernel.

Original Lean declaration header

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

theorem source_stein_identity_of_bounded_lipschitz_test {n : ℕ}
    {u f : EuclideanSpace ℝ (Fin n) → ℝ} {L G Lf : NNReal}
    (hu : ContDiff ℝ 1 u) (hL : LipschitzWith L u)
    (hG : LipschitzWith G (gradient u))
    (hnorm : (∫ y, Real.exp (-u y) ∂volume) = 1)
    (hf : ContDiff ℝ 1 f) (hfLip : LipschitzWith Lf f)
    (C : ℝ) (hbound : ∀ x, ‖f x‖ ≤ C) (i : Fin n) :
    Integrable (fun y => gradient u y i * f (gradient u y))
      ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u)) ∧
    Integrable (fun y => ∑ j, hessianMatrix u y i j * gradient f (gradient u y) j)
      ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u)) ∧
    (∫ y, gradient u y i * f (gradient u y)
      ∂((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u))) =
      ∫ y, (∑ j, hessianMatrix u y i j * gradient f (gradient u y) j)
        ∂((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u))

Module navigation

Module: KLS/LogConcave/HessianStein.

Definition modules: Analysis/BakryEmery/HessianOperator.

Supporting theorems: integral_fderiv_tilted_eq_integral_mul_fderiv_of_bounded_lipschitz, chain_coordinate_of_differentiableAt_gradient.

Next: source_affine_stein_identity_of_bounded_lipschitz_test.

Source excerpt, lines 234–248 · Frozen source 408915f.