gaussianReal_map_continuousLinearMap

English

The result holds for continuous linear maps as well: the Gaussian under L is Gaussian with mean L(μ) and variance (L 1)^2·v (to NNReal).

Русский

То же верно для непрерывно-линейных отображений: гауссиан сохраняется под L с тем же образом.

LaTeX

$$$ (GaussianReal(\mu,v)).map L = GaussianReal( L(\mu) , (L(1)^2).toNNReal \cdot v ). $$$

Lean4

theorem gaussianReal_map_continuousLinearMap (L : ℝ →L[ℝ] ℝ) :
    (gaussianReal μ v).map L = gaussianReal (L μ) ((L 1 ^ 2).toNNReal * v) :=
  gaussianReal_map_linearMap L

Похожие утверждения