English
Let E, F be real vector spaces and L: E →L[ℝ] F a continuous linear map. The pushforward under L commutes with convolution: (μ ∗ ν).map L = (μ.map L) ∗ (ν.map L).
Русский
Пусть E, F — вещественные векторные пространства, L: E →L[ℝ] F — непрерывный линейный отображение. Свёртка под L сочетаетcя со отображением: (μ ∗ ν).map L = (μ.map L) ∗ (ν.map L).
LaTeX
$$$(\\mu \\ast \\nu).map L = (\\mu.map L) \\ast (\\nu.map L)$$$
Lean4
theorem map_conv_continuousLinearMap {E F : Type*} [AddCommMonoid E] [AddCommMonoid F] [Module ℝ E] [Module ℝ F]
[TopologicalSpace E] [TopologicalSpace F] {mE : MeasurableSpace E} [MeasurableAdd₂ E] {mF : MeasurableSpace F}
[MeasurableAdd₂ F] [OpensMeasurableSpace E] [BorelSpace F] {μ ν : Measure E} [SFinite μ] [SFinite ν]
(L : E →L[ℝ] F) : (μ ∗ ν).map L = (μ.map L) ∗ (ν.map L) :=
by
suffices (μ ∗ ν).map (L : E →+ F) = (μ.map (L : E →+ F)) ∗ (ν.map (L : E →+ F)) by simpa
rw [map_conv_addMonoidHom]
rw [AddMonoidHom.coe_coe]
fun_prop
