Documentation
Atlas
.
BooleanFunctions
.
code
.
GaussianNoiseSemigroup
Search
return to top
source
Imports
Init
Atlas.BooleanFunctions.code.GaussianStability
Atlas.BooleanFunctions.code.OUSemigroup
Imported by
GaussianStability
.
gaussianNoiseOperator_eq_ornsteinUhlenbeckOp
source
theorem
GaussianStability
.
gaussianNoiseOperator_eq_ornsteinUhlenbeckOp
{
n
:
ℕ
}
(
ρ
:
ℝ
)
(
f
:
EuclideanSpace
ℝ
(
Fin
n
)
→
ℝ
)
:
gaussianNoiseOperator
ρ
f
=
GaussianSpace.ornsteinUhlenbeckOp
ρ
f