aemeasurable_fun_prod — Mathlib

English

If l is a list of functions with a.e.-measurable properties, then the product l.prod is a.e.-measurable with respect to μ.

Русский

Если в списке функции, измеримость которых верна almost everywhere, то их произведение измеримо almost everywhere.

LaTeX

$$$AEMeasurable l.prod\\mu$ при $\\forall f \\in l, AEMeasurable f \\mu$$$

Lean4

@[to_additive (attr := measurability, fun_prop)]
theorem aemeasurable_fun_prod (l : List (α → M)) (hl : ∀ f ∈ l, AEMeasurable f μ) :
    AEMeasurable (fun x => (l.map fun f : α → M => f x).prod) μ := by
  simpa only [← Pi.list_prod_apply] using l.aemeasurable_prod hl

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