English
If the group is commutative and μ is left-invariant and inv-invariant, the convolution is commutative: f ⋆ g = g ⋆ f.
Русский
Если группа коммутативна и μ слева инвариантна и инвариантна к обратному, свёртка коммутативна: f ⋆ g = g ⋆ f.
LaTeX
$$$[IsMulLeftInvariant \\mu] [IsInvInvariant \\mu] \\Rightarrow (f \\star_{μ} g) = (g \\star_{μ} f)$$$
Lean4
/-- Convolution is commutative when the group is commutative. -/
@[to_additive /-- Convolution is commutative when the group is commutative. -/
]
theorem mlconvolution_comm [IsMulLeftInvariant μ] [IsInvInvariant μ] {f g : G → ℝ≥0∞} : (f ⋆ₘₗ[μ] g) = (g ⋆ₘₗ[μ] f) :=
by
ext x
simp only [mlconvolution_def]
rw [← lintegral_mul_left_eq_self _ x, ← lintegral_inv_eq_self]
simp [mul_comm]
