mconv_zero — Mathlib

English

Convolution μ ∗ 0 is the zero measure.

Русский

Свёртка μ ∗ 0 равна нулевой мере.

LaTeX

$$$ μ ∗ 0 = 0 $$$

Lean4

/-- Convolution of a measure μ with the zero measure returns the zero measure. -/
@[to_additive (attr := simp) /-- Convolution of a measure μ with the zero measure returns the zero
    measure. -/
    ]
theorem mconv_zero (μ : Measure M) : μ ∗ₘ (0 : Measure M) = (0 : Measure M) :=
  by
  unfold mconv
  simp
    -- `mconv_smul_right` needs an instance to get `SFinite (c • ν)` from `SFinite ν`,
    -- hence it is placed in the `WithDensity` file, where the instance is defined.

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