convolutionExists_left — Mathlib

English

When the bilinear operator is scalar multiplication (i.e., the base field), the convolution reduces to (f ⋆ g)(x) = ∫ f(t) g(x − t) dt.

Русский

Если билинейный оператор — обычное умножение на скаляр, то свёртка сводится к (f⋆g)(x)=∫ f(t) g(x−t) dt.

LaTeX

$$$(f\\⋆[\\mathrm{mul},\\mu]\\ g)(x)=\\int t\\, f(t)\\, g(x-t)\\, d\\mu(t)$$$

Lean4

theorem _root_.HasCompactSupport.convolutionExists_left (hcf : HasCompactSupport f) (hf : Continuous f)
    (hg : LocallyIntegrable g μ) : ConvolutionExists f g L μ := fun x₀ =>
  convolutionExistsAt_flip.mp <| hcf.convolutionExists_right L.flip hg hf x₀

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