aestronglyMeasurable_fun_prod — Mathlib

English

If f is AEStronglyMeasurable, then g*f is AEStronglyMeasurable iff g is AEStronglyMeasurable (via commutativity).

Русский

Если f AEStronglyMeasurable, тогда g*f AEStronglyMeasurable тогда и только тогда, когда g AEStronglyMeasurable (через коммутативную группу).

LaTeX

$$$AEStronglyMeasurable\ f μ \rightarrow (AEStronglyMeasurable\ (g * f) μ \Leftrightarrow AEStronglyMeasurable\ g μ)$$$

Lean4

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

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