Gaussian Directional Integration by Parts

This statement gives Gaussian integration by parts for bounded globally Lipschitz $C^1$ tests.

Let $n\in\mathbb N$, let $s>0$, let $f:\mathbb R^n\to\mathbb R$ be $C^1$ and globally Lipschitz with Lipschitz constant represented by L : NNReal, and suppose there is $C\in\mathbb R$ such that $\|f(x)\|\le C$ for every $x$. For every $v\in\mathbb R^n$, both functions $x\mapsto\langle x,v\rangle f(x)$ and $x\mapsto D_vf(x)$ are integrable with respect to gaussianLaw s, and

This is the directional Gaussian identity with the exact parameterization used by gaussianLaw s, valid in all finite dimensions including $n=0$.

Original Lean declaration header

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

theorem gaussianLaw_directional_identity_of_bounded_lipschitz_test {n : ℕ}
    {s : ℝ} (hs : 0 < s) {f : EuclideanSpace ℝ (Fin n) → ℝ} {L : NNReal}
    (hf : ContDiff ℝ 1 f) (hLip : LipschitzWith L f) (C : ℝ) (hbound : ∀ x, ‖f x‖ ≤ C)
    (v : EuclideanSpace ℝ (Fin n)) :
    Integrable (fun x => ⟪x, v⟫ * f x) (gaussianLaw s) ∧
    Integrable (fun x => fderiv ℝ f x v) (gaussianLaw s) ∧
    (∫ x, ⟪x, v⟫ * f x ∂(gaussianLaw s)) =
      (2 * s)⁻¹ * ∫ x, fderiv ℝ f x v ∂(gaussianLaw s)

Module navigation

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

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

Supporting theorems: hasWeakDerivAlong_of_contDiff, integral_eq_zero_of_integrable_weak_derivative, gaussianLaw_exp_norm_integrable.

Previous: smoothedLaw_norm_sq · Next: gaussianLaw_translated_directional_identity_of_bounded_lipschitz_test.

Source excerpt, lines 409–416 · Frozen source 408915f.