stronglyMeasurable_prod_apply — Mathlib

English

Composable version for Finset of the product with an additional scalar argument, preserving strong measurability.

Русский

Композиционная версия для Finset; произведение с дополнительным скалярным аргументом сохраняет сильную измеримость.

LaTeX

$$$\forall s:\text{Finset } ι, \ (\forall i \in s, \text{StronglyMeasurable } (f i)) \Rightarrow \text{Measurable } g \Rightarrow \text{StronglyMeasurable } (a \mapsto \left(\prod_{i \in s} f i a\right) (g a))$$$

Lean4

/-- Compositional version of `Finset.stronglyMeasurable_prod` for use by `fun_prop`. -/
@[to_additive (attr := measurability, fun_prop) /--
    Compositional version of `Finset.stronglyMeasurable_sum` for use by `fun_prop`. -/
    ]
theorem stronglyMeasurable_prod_apply {ι : Type*} {f : ι → α → β → M} {g : α → β} {s : Finset ι}
    (hf : ∀ i ∈ s, StronglyMeasurable ↿(f i)) (hg : Measurable g) : StronglyMeasurable fun a ↦ (∏ i ∈ s, f i a) (g a) :=
  by simp only [Finset.prod_apply]; fun_prop (discharger := assumption)

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