mconv — Mathlib

English

On a discrete measurable space, the subtraction (or related binary operation) is measurable.

Русский

На дискретном пространстве измеримости операция вычитания (или аналогичная двусторонняя операция) измерима.

LaTeX

$$$\text{MeasurableSub₂}\,\alpha$$$

Lean4

/-- Multiplicative convolution of measures. -/
@[to_additive /-- Additive convolution of measures. -/
    ]
noncomputable def mconv (μ : Measure M) (ν : Measure M) : Measure M :=
  Measure.map (fun x : M × M ↦ x.1 * x.2) (μ.prod ν)

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