measurable_mlconvolution — Mathlib

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

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