Integrability of Source and Noise Stein Pairings

This statement establishes the integrability hypotheses for the Gaussian product coupling.

Let $n\in\mathbb N$. Let $u,h:\mathbb R^n\to\mathbb R$ be $C^1$ functions, with $u$ and $∇u$ globally Lipschitz, $∇u$ having Lipschitz constant G, and with

Let $h$ be globally Lipschitz and bounded by $C$, let $S$ be continuous linear, let $v\in\mathbb R^n$, and let $s>0$. On the product measure

with $Z(y,z)=S(∇u(y))+z$ and $F(y,z)=S(\operatorname{action}(\nabla^2u(y),S^*v))$, the theorem asserts that $Z$, $F$, $∇h\circ Z$ belong to MemLp · 2 P, and that the source pairing, noise pairing, Hessian pairing, and derivative pairing appearing in the product Stein identity are all integrable under $P$.

This is a technical integrability package supporting the subsequent product Stein identity.

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_pairings_integrable {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
      (gaussianLaw (V := EuclideanSpace ℝ (Fin n)) s)
    let Z := fun p : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) => S (gradient u p.1) + p.2
    let F := fun p : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) =>
      S (action (hessianMatrix u p.1) (S.adjoint v))
    MemLp Z 2 P ∧ MemLp F 2 P ∧ MemLp (fun p => gradient h (Z p)) 2 P ∧
    Integrable (fun p => ⟪S (gradient u p.1),v⟫ * h (Z p)) P ∧
    Integrable (fun p => ⟪p.2,v⟫ * h (Z p)) P ∧
    Integrable (fun p => ⟪S.adjoint v,action (hessianMatrix u p.1) (S.adjoint (gradient h (Z p)))⟫) P ∧
    Integrable (fun p => fderiv ℝ h (Z p) 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_exp_norm_integrable, norm_hessianMatrix_entry_le_of_lipschitz_gradient.

Next: gaussian_product_source_stein_identity.

Source excerpt, lines 36–55 · Frozen source 408915f.