sfinite_mconv_of_sfinite — Mathlib

English

The convolution of two s-finite measures is s-finite.

Русский

Свертка двух s‑конечных мер сохраняет свойство s‑конечности.

LaTeX

$$$ SFinite(\mu ∗ₘ ν) $$$

Lean4

/-- The convolution of s-finite measures is s-finite. -/
@[to_additive /-- The convolution of s-finite measures is s-finite. -/
    ]
instance sfinite_mconv_of_sfinite (μ : Measure M) (ν : Measure M) [SFinite μ] [SFinite ν] : SFinite (μ ∗ₘ ν) :=
  inferInstanceAs <| SFinite ((μ.prod ν).map fun (x : M × M) ↦ x.1 * x.2)

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