English
For any x ∈ M and a measure μ on M, the convolution (δ_x) ∗ μ equals the pushforward of μ by left multiplication by x: μ.map (y ↦ x·y).
Русский
Для любого x ∈ M и меры μ на M свертка δ_x ∗ μ равна образу меры μ при левом умножении на x: μ.map (y ↦ x·y).
LaTeX
$$$ (\delta_x) ∗ μ = μ \mapsto (y \mapsto x \cdot y) $$$
Lean4
@[to_additive]
theorem dirac_mconv [MeasurableMul₂ M] (x : M) (μ : Measure M) [SFinite μ] : (dirac x) ∗ₘ μ = μ.map (fun y ↦ x * y) :=
by
unfold mconv
rw [dirac_prod, map_map (by fun_prop) (by fun_prop)]
simp [Function.comp_def]