mconv_smul_left — Mathlib

English

For a scalar s ≥ 0, (s • μ) ∗ ν = s • (μ ∗ ν).

Русский

Для скаляра s ≥ 0 выполняется (s • μ) ∗ ν = s • (μ ∗ ν).

LaTeX

$$$ (s \cdot \mu) \ast_m \nu = s \cdot (\mu \ast_m \nu) $$$

Lean4

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

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