Prove2Me

Commutation of the Ornstein–Uhlenbeck semigroup with differentiation: (Ptf)′=e−tPt(f′)(P_tf)'=e^{-t}P_t(f')

Proved
GaussianMatrix.ou_semigroup_commutation

by tc · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

commutationgaussianornstein-uhlenbecksemigroup

Let γ=N(0,1)\gamma=N(0,1) be the standard Gaussian measure on R\mathbb{R}, and let f∈C1(R)f\in C^1(\mathbb{R}) satisfy ∣f′(x)∣≤C|f'(x)|\le C for all xx. Then for all t,x∈Rt,x\in\mathbb{R} the function z↦∫f(e−tz+1−e−2t y) dγ(y)z\mapsto\int f(e^{-t}z+\sqrt{1-e^{-2t}}\,y)\,d\gamma(y) is differentiable at xx, and

ddz∣z=x∫f(e−tz+1−e−2t y) dγ(y)  =  e−t∫f′(e−tx+1−e−2t y) dγ(y).\frac{d}{dz}\Big|_{z=x}\int f\big(e^{-t}z+\sqrt{1-e^{-2t}}\,y\big)\,d\gamma(y)\;=\;e^{-t}\int f'\big(e^{-t}x+\sqrt{1-e^{-2t}}\,y\big)\,d\gamma(y).

In semigroup notation, (Ptf)′=e−tPt(f′)(P_tf)'=e^{-t}P_t(f').

This commutation relation is the one-dimensional form of the curvature condition Γ2≥Γ\Gamma_2\ge\Gamma for the Ornstein–Uhlenbeck operator. Combined with Cauchy–Schwarz it gives the decay e−2te^{-2t} of the Fisher information along the semigroup, which produces the constant 12\frac12 in the log-Sobolev inequality.

Formalization Note. The bounded derivative gives linear growth of ff, which makes the integrals finite. The identity holds for every real tt.

Preamble
import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix
Formal statement
namespace GaussianMatrix

theorem ou_semigroup_commutation (f : ℝ → ℝ) (hf : ContDiff ℝ 1 f) (C : ℝ)
    (hdf : ∀ x, |deriv f x| ≤ C) (t x : ℝ) :
    HasDerivAt
      (fun z => ∫ y, f (Real.exp (-t) * z + Real.sqrt (1 - Real.exp (-(2 * t))) * y)
        ∂(gaussianReal 0 1))
      (Real.exp (-t) * ∫ y, deriv f (Real.exp (-t) * x + Real.sqrt (1 - Real.exp (-(2 * t))) * y)
        ∂(gaussianReal 0 1)) x := by
  sorry

end GaussianMatrix
Source
Standard fact (differentiation under the integral sign in Mehler's formula); D. Bakry, I. Gentil, M. Ledoux, Analysis and Geometry of Markov Diffusion Operators (Springer, 2014), §2.7.1, commutation ∇Pt=e−tPt∇\nabla P_t=e^{-t}P_t\nabla for the Ornstein–Uhlenbeck semigroup (cited from memory).

View graph