Translated Gaussian Directional Integration by Parts

This statement gives the translated form of Gaussian integration by parts.

Let $n\in\mathbb N$, let $h:\mathbb R^n\to\mathbb R$ be $C^1$ and globally Lipschitz, and suppose $\|h(x)\|\le C$ for every $x$. For $a,v\in\mathbb R^n$ and $s>0$, both functions $z\mapsto\langle z,v\rangle h(a+z)$ and $z\mapsto D_vh(a+z)$ are integrable with respect to gaussianLaw s, and

The result is a reusable translated-noise identity for product-coupling arguments.

Original Lean declaration header

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

theorem gaussianLaw_translated_directional_identity_of_bounded_lipschitz_test {n : ℕ}
    {h : EuclideanSpace ℝ (Fin n) → ℝ} {Lh : NNReal}
    (hh : ContDiff ℝ 1 h) (hhLip : LipschitzWith Lh h)
    (C : ℝ) (hbound : ∀ x, ‖h x‖ ≤ C)
    (a v : EuclideanSpace ℝ (Fin n)) {s : ℝ} (hs : 0 < s) :
    Integrable (fun z => ⟪z,v⟫ * h (a+z)) (gaussianLaw s) ∧
    Integrable (fun z => fderiv ℝ h (a+z) v) (gaussianLaw s) ∧
    (∫ z, ⟪z,v⟫ * h (a+z) ∂(gaussianLaw s)) =
      (2*s)⁻¹ * ∫ z, fderiv ℝ h (a+z) v ∂(gaussianLaw s)

Module navigation

Module: KLS/LogConcave/Density/GaussianSmoothing/Moments.

Definition modules: KLS/LogConcave/Density/GaussianSmoothing/Basic.

Supporting theorems: gaussianLaw_directional_identity_of_bounded_lipschitz_test.

Previous: gaussianLaw_directional_identity_of_bounded_lipschitz_test.

Source excerpt, lines 545–553 · Frozen source 408915f.