continuous_convolution_left — Mathlib

English

If f has compact support, f is continuous, and g is locally integrable, then the convolution f ⋆ g is continuous.

Русский

Если f имеет компактную поддержку, непрерывна, и g локально интегрируема, то свертка f ⋆ g непрерывна.

LaTeX

$$HasCompactSupport f → Continuous f → LocallyIntegrable g μ → Continuous (f ⋆[L, μ] g)$$

Lean4

theorem _root_.HasCompactSupport.continuous_convolution_left (hcf : HasCompactSupport f) (hf : Continuous f)
    (hg : LocallyIntegrable g μ) : Continuous (f ⋆[L, μ] g) :=
  by
  rw [← convolution_flip]
  exact hcf.continuous_convolution_right L.flip hg hf

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