English
The convolution of two real Gaussian distributions with means m1, m2 and variances v1, v2 is Gaussian with mean m1+m2 and variance v1+v2.
Русский
Свертка двух гауссианов с параметрами (m1,v1) и (m2,v2) даёт гауссиан с (m1+m2, v1+v2).
LaTeX
$$$ (\mathcal{N}(m_1,v_1) * \mathcal{N}(m_2,v_2)) = \mathcal{N}(m_1+m_2, v_1+v_2). $$$
Lean4
/-- The convolution of two real Gaussian distributions with means `m₁, m₂` and variances `v₁, v₂`
is a real Gaussian distribution with mean `m₁ + m₂` and variance `v₁ + v₂`. -/
theorem gaussianReal_conv_gaussianReal {m₁ m₂ : ℝ} {v₁ v₂ : ℝ≥0} :
(gaussianReal m₁ v₁) ∗ (gaussianReal m₂ v₂) = gaussianReal (m₁ + m₂) (v₁ + v₂) :=
by
refine Measure.ext_of_charFun ?_
ext t
simp_rw [charFun_conv, charFun_gaussianReal]
rw [← Complex.exp_add]
simp only [Complex.ofReal_add, NNReal.coe_add]
ring_nf
/- The sum of two real Gaussian variables with means `m₁, m₂` and variances `v₁, v₂` is a real
Gaussian distribution with mean `m₁ + m₂` and variance `v_1 + v_2`. -/
