Measurability of finite products and sums #
theorem
Finset.measurable_prod''
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
{M : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mM : MeasurableSpace M}
[CommMonoid M]
[MeasurableMul₂ M]
{f : ι → α → β → M}
{g : α → β}
{s : Finset ι}
(hf : ∀ i ∈ s, Measurable ↿(f i))
(hg : Measurable g)
:
Measurable fun (a : α) => (∏ i ∈ s, f i a) (g a)
Compositional version of Finset.measurable_prod for use by fun_prop.
theorem
Finset.measurable_sum''
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
{M : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mM : MeasurableSpace M}
[AddCommMonoid M]
[MeasurableAdd₂ M]
{f : ι → α → β → M}
{g : α → β}
{s : Finset ι}
(hf : ∀ i ∈ s, Measurable ↿(f i))
(hg : Measurable g)
:
Measurable fun (a : α) => (∑ i ∈ s, f i a) (g a)
Compositional version of Finset.measurable_sum for use by fun_prop.