aemeasurable_fun_prod — Mathlib

English

If s is a multiset of functions and each function is a.e.-measurable, then the function x ↦ (∏ f∈s f(x)) is a.e.-measurable with respect to μ.

Русский

Если s — мультисет функций и каждая функция a.e.-измерима, то x ↦ ∏ f∈s f(x) — a.e.-измерима.

LaTeX

$$$AEMeasurable (\\lambda x. (s.map (fun f => f x)).prod)\\mu$$$

Lean4

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

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