mlconvolution_zero — Mathlib

English

Convolution with the zero function yields the zero function: f ⋆ 0 = 0.

Русский

Свёртка с нулевой функцией даёт нулевую функцию: f ⋆ 0 = 0.

LaTeX

$$$f : G \\to \\mathbb{R}_{\\ge 0}^{\\infty},\\ μ : Measure G \\Rightarrow f \\star 0 = 0$$$

Lean4

/-- Convolution of a function with the zero function returns the zero function. -/
@[to_additive (attr := simp) /-- Convolution of a function with the zero function returns the zero function. -/
    ]
theorem mlconvolution_zero (f : G → ℝ≥0∞) (μ : Measure G) : f ⋆ₘₗ[μ] 0 = 0 := by ext; simp [mlconvolution]

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