mconv_dirac

Mathlib.MeasureTheory.Group.Convolution

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.mconv_dirac

← MathLib Explorer

English

Convolution μ ∗ δ_x equals μ.map (y ↦ y·x).

Русский

Свертка μ ∗ δ_x равна μ.map (y ↦ y·x).

LaTeX

$$$ μ \ast δ_x = μ.map (\lambda y. y \cdot x) $$$

Lean4

@[to_additive]
theorem mconv_dirac [MeasurableMul₂ M] (μ : Measure M) [SFinite μ] (x : M) : μ ∗ₘ (dirac x) = μ.map (fun y ↦ y * x) :=
  by
  unfold mconv
  rw [prod_dirac, map_map (by fun_prop) (by fun_prop)]
  simp [Function.comp_def]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru