Invariance of $N(0,1)$ under the Ornstein–Uhlenbeck semigroup: $\int P_th\,d\gamma=\int h\,d\gamma$

Proved

GaussianMatrix.ou_semigroup_invariant

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

gaussianinvariant-measureornstein-uhlenbecksemigroup

Let $\gamma=N(0,1)$ be the standard Gaussian measure on $\mathbb{R}$ , let $t\ge0$ , and let $h:\mathbb{R}\to\mathbb{R}$ be $\gamma$ -integrable. Then

\int\!\!\int h\big(e^{-t}x+\sqrt{1-e^{-2t}}\,y\big)\,d\gamma(y)\,d\gamma(x)\;=\;\int h\,d\gamma ,

that is, $\int P_th\,d\gamma=\int h\,d\gamma$ for the Ornstein–Uhlenbeck semigroup $P_t$ .

This expresses the invariance of $\gamma$ under $P_t$ . Equivalently, for independent standard Gaussians $X,Y$ and $a^2+b^2=1$ , the variable $aX+bY$ is standard Gaussian. It is used to bound the integrated Fisher information of $P_tf$ by $e^{-2t}$ times that of $f$ .

Formalization Note. The hypothesis $t\ge0$ is needed: for $t<0$ Lean's Real.sqrt of the negative number $1-e^{-2t}$ is $0$ , and the statement fails.

Preamble

import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix

Formal statement

namespace GaussianMatrix

theorem ou_semigroup_invariant (h : ℝ → ℝ) (hh : Integrable h (gaussianReal 0 1)) (t : ℝ)
    (ht : 0 ≤ t) :
    ∫ x, (∫ y, h (Real.exp (-t) * x + Real.sqrt (1 - Real.exp (-(2 * t))) * y)
        ∂(gaussianReal 0 1)) ∂(gaussianReal 0 1)
      = ∫ x, h x ∂(gaussianReal 0 1) := by
  sorry

end GaussianMatrix

Source

Standard fact: if

X,Y

are independent

N(0,1)

random variables and

a^2+b^2=1

then

aX+bY\sim N(0,1)

; hence

\gamma

is invariant for the Ornstein–Uhlenbeck semigroup. See D. Bakry, I. Gentil, M. Ledoux, Analysis and Geometry of Markov Diffusion Operators (Springer, 2014), §2.7.1 (cited from memory).

View graph

Invariance of N(0,1)N(0,1)N(0,1) under the Ornstein–Uhlenbeck semigroup: ∫Pth dγ=∫h dγ\int P_th\,d\gamma=\int h\,d\gamma∫Pt​hdγ=∫hdγ

Invariance of $N(0,1)$ under the Ornstein–Uhlenbeck semigroup: $\int P_th\,d\gamma=\int h\,d\gamma$