dirac_mconv_dirac — Mathlib

English

The convolution of two Dirac measures is the Dirac measure at the product: (δ_x) ∗ (δ_y) = δ_{x·y}.

Русский

Свертка двух дискретных Дирековских мер равна Дирековской мере в точке x·y.

LaTeX

$$$ (\delta_x) ∗ (\delta_y) = \delta_{x\cdot y} $$$

Lean4

@[to_additive (attr := simp)]
theorem dirac_mconv_dirac [MeasurableMul₂ M] (x y : M) : (dirac x) ∗ₘ (dirac y) = dirac (x * y) := by
  rw [mconv_dirac, map_dirac (by fun_prop)]

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