English
For monoids M, M' with measurable multiplications and μ, ν finite measures on M, and a monoid homomorphism L: M →* M', the pushforward of the convolution equals the convolution of pushes: (μ ∗ₘ ν).map L = (μ.map L) ∗ₘ (ν.map L).
Русский
Пусть есть моноиды M, M' с измеримыми операциями умножения и конечные меры μ, ν на M; при моноидному гомоморфизме L: M →* M' сопряжённая к L свёртка удовлетворяет (μ ∗ₘ ν).map L = (μ.map L) ∗ₘ (ν.map L).
LaTeX
$$$(\\mu \\ast_{m} \\nu).map L = (\\mu.map L) \\ast_{m} (\\nu.map L)$$$
Lean4
@[to_additive]
theorem map_mconv_monoidHom {M M' : Type*} {mM : MeasurableSpace M} [Monoid M] [MeasurableMul₂ M]
{mM' : MeasurableSpace M'} [Monoid M'] [MeasurableMul₂ M'] {μ ν : Measure M} [SFinite μ] [SFinite ν] (L : M →* M')
(hL : Measurable L) : (μ ∗ₘ ν).map L = (μ.map L) ∗ₘ (ν.map L) :=
by
unfold mconv
rw [map_map (by fun_prop) (by fun_prop)]
have : (L ∘ fun p : M × M ↦ p.1 * p.2) = (fun p : M' × M' ↦ p.1 * p.2) ∘ (Prod.map L L) := by ext; simp
rw [this, ← map_map (by fun_prop) (by fun_prop), ← map_prod_map _ _ (by fun_prop) (by fun_prop)]
