convolutionExistsAt_iff_integrable_swap

English

The convolution (f ⋆[L, μ] g) at a point x is defined by the integral ∫ L(f(t), g(x − t)) dμ(t).

Русский

Свёртка в точке x определяется как интеграл ∫ L(f(t), g(x − t)) dμ(t).

LaTeX

$$$(f\\ ⋆[L, μ]\\ g)(x)=\\int t\\, L(f(t),\, g(x-t))\\, dμ(t)$$$

Lean4

theorem convolutionExistsAt_iff_integrable_swap :
    ConvolutionExistsAt f g x L μ ↔ Integrable (fun t => L (f (x - t)) (g t)) μ :=
  convolutionExistsAt_flip.symm

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