Theorems · Theorem · probability

ProbabilityTheory.gaussianReal_conv_gaussianReal

∀ {m₁ m₂ : ℝ} {v₁ v₂ : NNReal},
  (ProbabilityTheory.gaussianReal m₁ v₁).conv (ProbabilityTheory.gaussianReal m₂ v₂) =
    ProbabilityTheory.gaussianReal (m₁ + m₂) (v₁ + v₂)

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₂.

Defined in: Mathlib.Probability.Distributions.Gaussian.Real
Cited by: 1 results in Mathlib
Foundations: Depth 295 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
MeasureTheory.Measurestatement · cited by 10,939
Complexproof · cited by 5,565
NNRealstatement and proof · cited by 4,310
mul_oneproof · cited by 3,885
add_zeroproof · cited by 2,707
Complex.ofRealproof · cited by 1,654
NNReal.toRealproof · cited by 1,260
pow_oneproof · cited by 894
Complex.Iproof · cited by 866
Complex.expproof · cited by 612
Complex.ofReal_addproof · cited by 94

Cited by1

Results whose statement or proof uses this declaration.

ProbabilityTheory.gaussianReal_add_gaussianReal_of_indepFunproof · cited by 0