aemeasurable_mlconvolution — Mathlib

English

If f and g are AEMeasurable with respect to μ, then f ⋆ g is AEMeasurable.

Русский

Если f и g AEMеасurable по отношению к μ, то f ⋆ g AEMеасurable.

LaTeX

$$$f,g: G \\to \\mathbb{R}_{\\ge 0}^{\\infty},\\ hf : AEMeasurable f μ,\\ hg : AEMeasurable g μ \\Rightarrow AEMeasurable (f \\star_{μ} g) μ$$$

Lean4

/-- The convolution of `AEMeasurable` functions is `AEMeasurable`. -/
@[to_additive (attr := measurability, fun_prop) /-- The convolution of `AEMeasurable` functions is `AEMeasurable`. -/
    ]
theorem aemeasurable_mlconvolution {f g : G → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    AEMeasurable (f ⋆ₘₗ[μ] g) μ := by
  unfold mlconvolution
  fun_prop

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