probabilitymeasure_of_probabilitymeasures_mconv

English

If μ and ν are probability measures on a monoid M with measurable multiplication, then their convolution μ ∗ₘ ν is again a probability measure.

Русский

Если μ и ν — распределения вероятности на моноиде M с измеримой операцией умножения, то их свёртка μ ∗ₘ ν снова является распределением вероятности.

LaTeX

$$$\\operatorname{IsProbabilityMeasure}(\\mu \\ast_{m} \\nu)$$$

Lean4

@[to_additive]
instance probabilitymeasure_of_probabilitymeasures_mconv (μ : Measure M) (ν : Measure M) [MeasurableMul₂ M]
    [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] : IsProbabilityMeasure (μ ∗ₘ ν) :=
  isProbabilityMeasure_map (by fun_prop)

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