mconv_smul_right — Mathlib

English

On a group G with left-invariant measure μ, for AEMeasurable f,g: G→ℝ≥0∞, μ_f ∗ μ_g = μ_{mlconvolution(f,g)}.

Русский

На группе G с лево-инвариантной мерой μ для плотностей f,g: G→ℝ≥0∞ выполняется μ_f ∗ μ_g = μ_{mlconvolution(f,g)}.

LaTeX

$$$ μ^{f} *_{μ} μ^{g} = μ^{(f \star_{μ} g)} $$$

Lean4

@[to_additive conv_smul_right]
theorem mconv_smul_right (μ : Measure M) (ν : Measure M) [SFinite ν] (s : ℝ≥0∞) : μ ∗ₘ (s • ν) = s • (μ ∗ₘ ν) :=
  by
  unfold mconv
  rw [Measure.prod_smul_right, Measure.map_smul]

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