convolution_zero — Mathlib

English

If one input function is continuous and the other is integrable, the convolution is well-defined and respects continuity in the appropriate sense.

Русский

Если одна функция непрерывна, другая интегрируема, свёртка корректно определена и сохраняет непрерывность по месту определения.

LaTeX

$$$\\mathrm{ConvolutionExists}(f,g,L,μ)\\Rightarrow \\text{continuity in appropriate sense}$$$

Lean4

@[simp]
theorem convolution_zero : f ⋆[L, μ] 0 = 0 := by
  ext
  simp_rw [convolution_def, Pi.zero_apply, (L _).map_zero, integral_zero]

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