aemeasurable_prod — Mathlib

English

If l is a list of functions with measurable members, then the product l.prod is measurable.

Русский

Если список функций содержит измеримые элементы, то их попарное произведение измеримо.

LaTeX

$$$\\text{Measurable } l.prod$ при $\\forall f \\in l,\\ Measurable f$$$

Lean4

@[to_additive (attr := measurability, fun_prop)]
theorem aemeasurable_prod (l : List (α → M)) (hl : ∀ f ∈ l, AEMeasurable f μ) : AEMeasurable l.prod μ := by
  induction l with
  | nil => exact aemeasurable_one
  | cons f l ihl =>
    rw [List.forall_mem_cons] at hl
    rw [List.prod_cons]
    exact hl.1.mul (ihl hl.2)

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