English
Let M be a monoid with a measurable multiplication, and μ, ν, ρ be measures on M with ν and ρ finite (SFinite). Then the convolution is associative: (μ ∗ₘ ν) ∗ₘ ρ = μ ∗ₘ (ν ∗ₘ ρ).
Русский
Пусть M — моноид с измеримой операцией умножения, а μ, ν, ρ — меры на M; если ν и ρ конечны, то свёртка тождественна слева: (μ ∗ₘ ν) ∗ₘ ρ = μ ∗ₘ (ν ∗ₘ ρ).
LaTeX
$$$(\\mu \\ast_{m} \\nu) \\ast_{m} \\rho = \\mu \\ast_{m} (\\nu \\ast_{m} \\rho)$$$
Lean4
/-- Convolution is associative. -/
@[to_additive /-- Convolution is associative. -/
]
theorem mconv_assoc [MeasurableMul₂ M] (μ ν ρ : Measure M) [SFinite ν] [SFinite ρ] : (μ ∗ₘ ν) ∗ₘ ρ = μ ∗ₘ (ν ∗ₘ ρ) :=
by
refine ext_of_lintegral _ fun f hf ↦ ?_
repeat rw [lintegral_mconv (by fun_prop)]
refine lintegral_congr fun x ↦ ?_
rw [lintegral_mconv (by fun_prop)]
repeat refine lintegral_congr fun x ↦ ?_
simp [mul_assoc]
