dirac_mconv — Mathlib

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]

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