Gaussian Product Source Stein Identity

This statement combines the affine source identity with the translated Gaussian identity on a product coupling.

Let $n\in\mathbb N$, let $u,h:\mathbb R^n\to\mathbb R$ be $C^1$, with $u$ and $∇u$ globally Lipschitz, and assume $\int e^{-u}=1$. Let $h$ be globally Lipschitz and bounded by $C$, let $S$ be continuous linear, let $v\in\mathbb R^n$, and let $s>0$. Define

Then the two displayed functions are integrable under $P$, and

This is the exact product-coupling identity and includes all stated integrability conclusions.

Original Lean declaration header

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

set_option maxHeartbeats 800000 in
theorem gaussian_product_source_stein_identity {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))
    (v : EuclideanSpace ℝ (Fin n)) {s : ℝ} (hs : 0 < s) :
    let P := ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u)).prod
      (FunctionalInequalities.KLS.LogConcave.GaussianSmoothing.gaussianLaw (V := EuclideanSpace ℝ (Fin n)) s)
    Integrable (fun p : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) =>
      ⟪S (gradient u p.1) + p.2, v⟫ * h (S (gradient u p.1) + p.2)) P ∧
    Integrable (fun p : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) =>
      ⟪S.adjoint v, action (hessianMatrix u p.1)
        (S.adjoint (gradient h (S (gradient u p.1) + p.2)))⟫ +
          (2 * s)⁻¹ * fderiv ℝ h (S (gradient u p.1) + p.2) v) P ∧
    (∫ p : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n),
      ⟪S (gradient u p.1) + p.2, v⟫ * h (S (gradient u p.1) + p.2) ∂P) =
      ∫ p : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n),
        ⟪S.adjoint v, action (hessianMatrix u p.1)
          (S.adjoint (gradient h (S (gradient u p.1) + p.2)))⟫ +
            (2 * s)⁻¹ * fderiv ℝ h (S (gradient u p.1) + p.2) v ∂P

Module navigation

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

Definition modules: Analysis/BakryEmery/HessianOperator, KLS/LogConcave/Density/GaussianSmoothing/Basic, Probability/Stein/Kernel.

Supporting theorems: gaussianLaw_translated_directional_identity_of_bounded_lipschitz_test, gaussian_product_source_stein_pairings_integrable, source_affine_stein_identity_of_bounded_lipschitz_test.

Previous: gaussian_product_source_stein_pairings_integrable · Next: gaussian_product_compact_dual_bound.

Source excerpt, lines 124–147 · Frozen source 408915f.