dirac_one_mconv — Mathlib

English

Convolution with the Dirac measure at 1 leaves the measure unchanged: (δ_1) ∗ μ = μ.

Русский

Свёртка Дирцевой меры в точке 1 оставляет меру неизменной.

LaTeX

$$$ (\delta_1) ∗ μ = μ $$$

Lean4

/-- Convolution of the dirac measure at 1 with a measure μ returns μ. -/
@[to_additive (attr := simp) /-- Convolution of the dirac measure at 0 with a measure μ returns μ. -/
    ]
theorem dirac_one_mconv [MeasurableMul₂ M] (μ : Measure M) [SFinite μ] : (dirac 1) ∗ₘ μ = μ := by simp [dirac_mconv]

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