English
For a scalar bilinear map, the same symmetry of convolution holds: convolution with lsmul equals the integral of f(x−t) times g(t).
Русский
Для билинейной формы скалярного типа та же симметрия свёртки: свёртка через lsmul равна интегралу f(x−t) умноженного на g(t).
LaTeX
$$$ (f ⋆[lsmul 𝕜 𝕜, μ] g)(x) = \int_G f(x-t) \cdot g(t) \, dμ(t). $$$
Lean4
/-- The convolution of two even functions is also even. -/
theorem convolution_neg_of_neg_eq (h1 : ∀ᵐ x ∂μ, f (-x) = f x) (h2 : ∀ᵐ x ∂μ, g (-x) = g x) :
(f ⋆[L, μ] g) (-x) = (f ⋆[L, μ] g) x :=
calc
∫ t : G, (L (f t)) (g (-x - t)) ∂μ = ∫ t : G, (L (f (-t))) (g (x + t)) ∂μ :=
by
apply integral_congr_ae
filter_upwards [h1, (eventually_add_left_iff μ x).2 h2] with t ht h't
simp_rw [ht, ← h't, neg_add']
_ = ∫ t : G, (L (f t)) (g (x - t)) ∂μ := by
rw [← integral_neg_eq_self]
simp only [neg_neg, ← sub_eq_add_neg]
