convolution_flip — Mathlib

English

The symmetric definition of convolution with multiplication: (f ⋆[mul 𝕜 𝕜, μ] g)(x) = ∫ f(x−t) g(t) dμ.

Русский

Симметричное определение свёртки с умножением: (f ⋆[mul 𝕜 𝕜, μ] g)(x) = ∫ f(x−t) g(t) dμ.

LaTeX

$$$(f ⋆[mul 𝕜 𝕜, μ] g)(x) = \int_G f(x-t) \cdot g(t) \, d\mu(t).$$$

Lean4

/-- Commutativity of convolution -/
theorem convolution_flip : g ⋆[L.flip, μ] f = f ⋆[L, μ] g :=
  by
  ext1 x
  simp_rw [convolution_def]
  rw [← integral_sub_left_eq_self _ μ x]
  simp_rw [sub_sub_self, flip_apply]

Похожие утверждения