mconv_withDensity_eq_mlconvolution

English

On measures μ,ν on a monoid M, μ ∗ₘ (s • ν) = s • (μ ∗ₘ ν) for s ∈ ℝ≥0∞ when ν is SFinite.

Русский

Для мер μ,ν на моноиде M выполняется μ ∗ₘ (s • ν) = s • (μ ∗ₘ ν) при s ∈ ℝ≥0∞ и ν ∈ SFinite.

LaTeX

$$$ μ ∗ₘ (s \cdot ν) = s \cdot (μ ∗ₘ ν)$$$

Lean4

@[to_additive]
theorem mconv_withDensity_eq_mlconvolution {f g : G → ℝ≥0∞} (hf : Measurable f) (hg : Measurable g) :
    μ.withDensity f ∗ₘ μ.withDensity g = μ.withDensity (f ⋆ₘₗ[μ] g) :=
  mconv_withDensity_eq_mlconvolution₀ hf.aemeasurable hg.aemeasurable

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