English
If f and g are measurable, then their mlconvolution is measurable.
Русский
Если f и g измеримы, то их свёртка измерима.
LaTeX
$$$f,g:\\, G \\to \\mathbb{R}_{\\ge 0}^{\\infty},\\ hf : Measurable f,\\ hg : Measurable g \\Rightarrow Measurable (f \\star_{\\mu} g)$$$
Lean4
/-- The convolution of measurable functions is measurable. -/
@[to_additive (attr := measurability, fun_prop) /-- The convolution of measurable functions is measurable. -/
]
theorem measurable_mlconvolution {f g : G → ℝ≥0∞} (μ : Measure G) [SFinite μ] (hf : Measurable f) (hg : Measurable g) :
Measurable (f ⋆ₘₗ[μ] g) := by
unfold mlconvolution
fun_prop