aestronglyMeasurable_prod — Mathlib

English

If f is AEStronglyMeasurable, then f*g is AEStronglyMeasurable iff g is AEStronglyMeasurable (under commutative group).

Русский

Если f является AEStronglyMeasurable, тогда f·g AEStronglyMeasurable тогда и только тогда, когда g AEStronglyMeasurable (при коммутативной группе).

LaTeX

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

Lean4

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

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