mathlib documentation

measure_theory.arithmetic

Typeclasses for measurability of operations #

In this file we define classes has_measurable_mul etc and prove dot-style lemmas (measurable.mul, ae_measurable.mul etc). For binary operations we define two typeclasses:

and similarly for other binary operations. The reason for introducing these classes is that in case of topological space α equipped with the Borel σ-algebra, instances for has_measurable_mul₂ etc require α to have a second countable topology.

We define separate classes for has_measurable_div/has_measurable_sub because on some types (e.g., , ℝ≥0∞) division and/or subtraction are not defined as a * b⁻¹ / a + (-b).

For instances relating, e.g., has_continuous_mul to has_measurable_mul see file measure_theory.borel_space.

Tags #

measurable function, arithmetic operator

Binary operations: (+), (*), (-), (/) #

@[class]
structure has_measurable_add (M : Type u_2) [measurable_space M] [has_add M] :
Prop

We say that a type has_measurable_add if ((+) c) and (+ c) are measurable functions. For a typeclass assuming measurability of uncurry (+) see has_measurable_add₂.

Instances
@[class]
structure has_measurable_add₂ (M : Type u_2) [measurable_space M] [has_add M] :
Prop

We say that a type has_measurable_add if uncurry (+) is a measurable functions. For a typeclass assuming measurability of ((+) c) and (+ c) see has_measurable_add.

Instances
@[class]
structure has_measurable_mul (M : Type u_2) [measurable_space M] [has_mul M] :
Prop

We say that a type has_measurable_mul if ((*) c) and (* c) are measurable functions. For a typeclass assuming measurability of uncurry (*) see has_measurable_mul₂.

Instances
@[class]
structure has_measurable_mul₂ (M : Type u_2) [measurable_space M] [has_mul M] :
Prop

We say that a type has_measurable_mul if uncurry (*) is a measurable functions. For a typeclass assuming measurability of ((*) c) and (* c) see has_measurable_mul.

Instances
theorem measurable.add {α : Type u_1} [measurable_space α] {M : Type u_2} [measurable_space M] [has_add M] [has_measurable_add₂ M] {f g : α → M} (hf : measurable f) (hg : measurable g) :
measurable (λ (a : α), f a + g a)
theorem measurable.mul {α : Type u_1} [measurable_space α] {M : Type u_2} [measurable_space M] [has_mul M] [has_measurable_mul₂ M] {f g : α → M} (hf : measurable f) (hg : measurable g) :
measurable (λ (a : α), (f a) * g a)
theorem ae_measurable.add {α : Type u_1} [measurable_space α] {M : Type u_2} [measurable_space M] [has_add M] [has_measurable_add₂ M] {μ : measure_theory.measure α} {f g : α → M} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (a : α), f a + g a) μ
theorem ae_measurable.mul {α : Type u_1} [measurable_space α] {M : Type u_2} [measurable_space M] [has_mul M] [has_measurable_mul₂ M] {μ : measure_theory.measure α} {f g : α → M} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (a : α), (f a) * g a) μ
theorem measurable.const_add {α : Type u_1} [measurable_space α] {M : Type u_2} [measurable_space M] [has_add M] [has_measurable_add M] {f : α → M} (hf : measurable f) (c : M) :
measurable (λ (x : α), c + f x)
theorem measurable.const_mul {α : Type u_1} [measurable_space α] {M : Type u_2} [measurable_space M] [has_mul M] [has_measurable_mul M] {f : α → M} (hf : measurable f) (c : M) :
measurable (λ (x : α), c * f x)
theorem ae_measurable.const_mul {α : Type u_1} [measurable_space α] {M : Type u_2} [measurable_space M] [has_mul M] [has_measurable_mul M] {f : α → M} {μ : measure_theory.measure α} (hf : ae_measurable f μ) (c : M) :
ae_measurable (λ (x : α), c * f x) μ
theorem ae_measurable.const_add {α : Type u_1} [measurable_space α] {M : Type u_2} [measurable_space M] [has_add M] [has_measurable_add M] {f : α → M} {μ : measure_theory.measure α} (hf : ae_measurable f μ) (c : M) :
ae_measurable (λ (x : α), c + f x) μ
theorem measurable.add_const {α : Type u_1} [measurable_space α] {M : Type u_2} [measurable_space M] [has_add M] [has_measurable_add M] {f : α → M} (hf : measurable f) (c : M) :
measurable (λ (x : α), f x + c)
theorem measurable.mul_const {α : Type u_1} [measurable_space α] {M : Type u_2} [measurable_space M] [has_mul M] [has_measurable_mul M] {f : α → M} (hf : measurable f) (c : M) :
measurable (λ (x : α), (f x) * c)
theorem ae_measurable.mul_const {α : Type u_1} [measurable_space α] {M : Type u_2} [measurable_space M] [has_mul M] [has_measurable_mul M] {f : α → M} {μ : measure_theory.measure α} (hf : ae_measurable f μ) (c : M) :
ae_measurable (λ (x : α), (f x) * c) μ
theorem ae_measurable.add_const {α : Type u_1} [measurable_space α] {M : Type u_2} [measurable_space M] [has_add M] [has_measurable_add M] {f : α → M} {μ : measure_theory.measure α} (hf : ae_measurable f μ) (c : M) :
ae_measurable (λ (x : α), f x + c) μ
@[class]
structure has_measurable_pow (β : Type u_2) (γ : Type u_3) [measurable_space β] [measurable_space γ] [has_pow β γ] :
Type

This class assumes that the map β × γ → β given by (x, y) ↦ x ^ y is measurable.

Instances
theorem measurable.pow {α : Type u_1} [measurable_space α] {β : Type u_2} {γ : Type u_3} [measurable_space β] [measurable_space γ] [has_pow β γ] [has_measurable_pow β γ] {f : α → β} {g : α → γ} (hf : measurable f) (hg : measurable g) :
measurable (λ (x : α), f x ^ g x)
theorem ae_measurable.pow {α : Type u_1} [measurable_space α] {β : Type u_2} {γ : Type u_3} [measurable_space β] [measurable_space γ] [has_pow β γ] [has_measurable_pow β γ] {μ : measure_theory.measure α} {f : α → β} {g : α → γ} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (x : α), f x ^ g x) μ
theorem measurable.pow_const {α : Type u_1} [measurable_space α] {β : Type u_2} {γ : Type u_3} [measurable_space β] [measurable_space γ] [has_pow β γ] [has_measurable_pow β γ] {f : α → β} (hf : measurable f) (c : γ) :
measurable (λ (x : α), f x ^ c)
theorem ae_measurable.pow_const {α : Type u_1} [measurable_space α] {β : Type u_2} {γ : Type u_3} [measurable_space β] [measurable_space γ] [has_pow β γ] [has_measurable_pow β γ] {μ : measure_theory.measure α} {f : α → β} (hf : ae_measurable f μ) (c : γ) :
ae_measurable (λ (x : α), f x ^ c) μ
theorem measurable.const_pow {α : Type u_1} [measurable_space α] {β : Type u_2} {γ : Type u_3} [measurable_space β] [measurable_space γ] [has_pow β γ] [has_measurable_pow β γ] {f : α → γ} (hf : measurable f) (c : β) :
measurable (λ (x : α), c ^ f x)
theorem ae_measurable.const_pow {α : Type u_1} [measurable_space α] {β : Type u_2} {γ : Type u_3} [measurable_space β] [measurable_space γ] [has_pow β γ] [has_measurable_pow β γ] {μ : measure_theory.measure α} {f : α → γ} (hf : ae_measurable f μ) (c : β) :
ae_measurable (λ (x : α), c ^ f x) μ
@[class]
structure has_measurable_sub (G : Type u_2) [measurable_space G] [has_sub G] :
Prop
  • measurable_const_sub : ∀ (c : G), measurable (λ (x : G), c - x)
  • measurable_sub_const : ∀ (c : G), measurable (λ (x : G), x - c)

We say that a type has_measurable_sub if (λ x, c - x) and (λ x, x - c) are measurable functions. For a typeclass assuming measurability of uncurry (-) see has_measurable_sub₂.

Instances
@[class]
structure has_measurable_sub₂ (G : Type u_2) [measurable_space G] [has_sub G] :
Prop

We say that a type has_measurable_sub if uncurry (-) is a measurable functions. For a typeclass assuming measurability of ((-) c) and (- c) see has_measurable_sub.

Instances
@[class]
structure has_measurable_div (G₀ : Type u_2) [measurable_space G₀] [has_div G₀] :
Prop

We say that a type has_measurable_div if ((/) c) and (/ c) are measurable functions. For a typeclass assuming measurability of uncurry (/) see has_measurable_div₂.

Instances
@[class]
structure has_measurable_div₂ (G₀ : Type u_2) [measurable_space G₀] [has_div G₀] :
Prop

We say that a type has_measurable_div if uncurry (/) is a measurable functions. For a typeclass assuming measurability of ((/) c) and (/ c) see has_measurable_div.

Instances
theorem measurable.div {α : Type u_1} [measurable_space α] {G : Type u_2} [measurable_space G] [has_div G] [has_measurable_div₂ G] {f g : α → G} (hf : measurable f) (hg : measurable g) :
measurable (λ (a : α), f a / g a)
theorem measurable.sub {α : Type u_1} [measurable_space α] {G : Type u_2} [measurable_space G] [has_sub G] [has_measurable_sub₂ G] {f g : α → G} (hf : measurable f) (hg : measurable g) :
measurable (λ (a : α), f a - g a)
theorem ae_measurable.sub {α : Type u_1} [measurable_space α] {G : Type u_2} [measurable_space G] [has_sub G] [has_measurable_sub₂ G] {f g : α → G} {μ : measure_theory.measure α} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (a : α), f a - g a) μ
theorem ae_measurable.div {α : Type u_1} [measurable_space α] {G : Type u_2} [measurable_space G] [has_div G] [has_measurable_div₂ G] {f g : α → G} {μ : measure_theory.measure α} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (a : α), f a / g a) μ
theorem measurable.const_div {α : Type u_1} [measurable_space α] {G : Type u_2} [measurable_space G] [has_div G] [has_measurable_div G] {f : α → G} (hf : measurable f) (c : G) :
measurable (λ (x : α), c / f x)
theorem measurable.const_sub {α : Type u_1} [measurable_space α] {G : Type u_2} [measurable_space G] [has_sub G] [has_measurable_sub G] {f : α → G} (hf : measurable f) (c : G) :
measurable (λ (x : α), c - f x)
theorem ae_measurable.const_sub {α : Type u_1} [measurable_space α] {G : Type u_2} [measurable_space G] [has_sub G] [has_measurable_sub G] {f : α → G} {μ : measure_theory.measure α} (hf : ae_measurable f μ) (c : G) :
ae_measurable (λ (x : α), c - f x) μ
theorem ae_measurable.const_div {α : Type u_1} [measurable_space α] {G : Type u_2} [measurable_space G] [has_div G] [has_measurable_div G] {f : α → G} {μ : measure_theory.measure α} (hf : ae_measurable f μ) (c : G) :
ae_measurable (λ (x : α), c / f x) μ
theorem measurable.sub_const {α : Type u_1} [measurable_space α] {G : Type u_2} [measurable_space G] [has_sub G] [has_measurable_sub G] {f : α → G} (hf : measurable f) (c : G) :
measurable (λ (x : α), f x - c)
theorem measurable.div_const {α : Type u_1} [measurable_space α] {G : Type u_2} [measurable_space G] [has_div G] [has_measurable_div G] {f : α → G} (hf : measurable f) (c : G) :
measurable (λ (x : α), f x / c)
theorem ae_measurable.sub_const {α : Type u_1} [measurable_space α] {G : Type u_2} [measurable_space G] [has_sub G] [has_measurable_sub G] {f : α → G} {μ : measure_theory.measure α} (hf : ae_measurable f μ) (c : G) :
ae_measurable (λ (x : α), f x - c) μ
theorem ae_measurable.div_const {α : Type u_1} [measurable_space α] {G : Type u_2} [measurable_space G] [has_div G] [has_measurable_div G] {f : α → G} {μ : measure_theory.measure α} (hf : ae_measurable f μ) (c : G) :
ae_measurable (λ (x : α), f x / c) μ
@[class]
structure has_measurable_neg (G : Type u_2) [has_neg G] [measurable_space G] :
Prop

We say that a type has_measurable_neg if x ↦ -x is a measurable function.

Instances
@[class]
structure has_measurable_inv (G : Type u_2) [has_inv G] [measurable_space G] :
Prop

We say that a type has_measurable_inv if x ↦ x⁻¹ is a measurable function.

Instances
theorem measurable.inv {α : Type u_1} [measurable_space α] {G : Type u_2} [has_inv G] [measurable_space G] [has_measurable_inv G] {f : α → G} (hf : measurable f) :
measurable (λ (x : α), (f x)⁻¹)
theorem measurable.neg {α : Type u_1} [measurable_space α] {G : Type u_2} [has_neg G] [measurable_space G] [has_measurable_neg G] {f : α → G} (hf : measurable f) :
measurable (λ (x : α), -f x)
theorem ae_measurable.neg {α : Type u_1} [measurable_space α] {G : Type u_2} [has_neg G] [measurable_space G] [has_measurable_neg G] {f : α → G} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :
ae_measurable (λ (x : α), -f x) μ
theorem ae_measurable.inv {α : Type u_1} [measurable_space α] {G : Type u_2} [has_inv G] [measurable_space G] [has_measurable_inv G] {f : α → G} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :
ae_measurable (λ (x : α), (f x)⁻¹) μ
@[simp]
theorem measurable_inv_iff {α : Type u_1} [measurable_space α] {G : Type u_2} [group G] [measurable_space G] [has_measurable_inv G] {f : α → G} :
measurable (λ (x : α), (f x)⁻¹) measurable f
@[simp]
theorem measurable_neg_iff {α : Type u_1} [measurable_space α] {G : Type u_2} [add_group G] [measurable_space G] [has_measurable_neg G] {f : α → G} :
measurable (λ (x : α), -f x) measurable f
@[simp]
theorem ae_measurable_inv_iff {α : Type u_1} [measurable_space α] {G : Type u_2} [group G] [measurable_space G] [has_measurable_inv G] {f : α → G} {μ : measure_theory.measure α} :
ae_measurable (λ (x : α), (f x)⁻¹) μ ae_measurable f μ
@[simp]
theorem ae_measurable_neg_iff {α : Type u_1} [measurable_space α] {G : Type u_2} [add_group G] [measurable_space G] [has_measurable_neg G] {f : α → G} {μ : measure_theory.measure α} :
ae_measurable (λ (x : α), -f x) μ ae_measurable f μ
@[simp]
theorem measurable_inv_iff' {α : Type u_1} [measurable_space α] {G₀ : Type u_2} [group_with_zero G₀] [measurable_space G₀] [has_measurable_inv G₀] {f : α → G₀} :
measurable (λ (x : α), (f x)⁻¹) measurable f
@[simp]
theorem ae_measurable_inv_iff' {α : Type u_1} [measurable_space α] {G₀ : Type u_2} [group_with_zero G₀] [measurable_space G₀] [has_measurable_inv G₀] {f : α → G₀} {μ : measure_theory.measure α} :
ae_measurable (λ (x : α), (f x)⁻¹) μ ae_measurable f μ
@[instance]
Equations
@[class]
structure has_measurable_smul (M : Type u_2) (α : Type u_3) [has_scalar M α] [measurable_space M] [measurable_space α] :
Prop

We say that the action of M on α has_measurable_smul if for each c the map x ↦ c • x is a measurable function and for each x the map c ↦ c • x is a measurable function.

Instances
@[class]
structure has_measurable_smul₂ (M : Type u_2) (α : Type u_3) [has_scalar M α] [measurable_space M] [measurable_space α] :
Prop

We say that the action of M on α has_measurable_smul if the map (c, x) ↦ c • x is a measurable function.

Instances
theorem measurable.smul {α : Type u_1} [measurable_space α] {M : Type u_2} {β : Type u_3} [measurable_space M] [measurable_space β] [has_scalar M β] [has_measurable_smul₂ M β] {f : α → M} {g : α → β} (hf : measurable f) (hg : measurable g) :
measurable (λ (x : α), f x g x)
theorem ae_measurable.smul {α : Type u_1} [measurable_space α] {M : Type u_2} {β : Type u_3} [measurable_space M] [measurable_space β] [has_scalar M β] [has_measurable_smul₂ M β] {f : α → M} {g : α → β} {μ : measure_theory.measure α} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (x : α), f x g x) μ
theorem measurable.smul_const {α : Type u_1} [measurable_space α] {M : Type u_2} {β : Type u_3} [measurable_space M] [measurable_space β] [has_scalar M β] [has_measurable_smul M β] {f : α → M} (hf : measurable f) (y : β) :
measurable (λ (x : α), f x y)
theorem ae_measurable.smul_const {α : Type u_1} [measurable_space α] {M : Type u_2} {β : Type u_3} [measurable_space M] [measurable_space β] [has_scalar M β] [has_measurable_smul M β] {μ : measure_theory.measure α} {f : α → M} (hf : ae_measurable f μ) (y : β) :
ae_measurable (λ (x : α), f x y) μ
theorem measurable.const_smul' {α : Type u_1} [measurable_space α] {M : Type u_2} {β : Type u_3} [measurable_space M] [measurable_space β] [has_scalar M β] [has_measurable_smul M β] {f : α → β} (hf : measurable f) (c : M) :
measurable (λ (x : α), c f x)
theorem measurable.const_smul {α : Type u_1} [measurable_space α] {M : Type u_2} {β : Type u_3} [measurable_space M] [measurable_space β] [has_scalar M β] [has_measurable_smul M β] {f : α → β} (hf : measurable f) (c : M) :
theorem ae_measurable.const_smul' {α : Type u_1} [measurable_space α] {M : Type u_2} {β : Type u_3} [measurable_space M] [measurable_space β] [has_scalar M β] [has_measurable_smul M β] {μ : measure_theory.measure α} {f : α → β} (hf : ae_measurable f μ) (c : M) :
ae_measurable (λ (x : α), c f x) μ
theorem ae_measurable.const_smul {α : Type u_1} [measurable_space α] {M : Type u_2} {β : Type u_3} [measurable_space M] [measurable_space β] [has_scalar M β] [has_measurable_smul M β] {μ : measure_theory.measure α} {f : α → β} (hf : ae_measurable f μ) (c : M) :
@[simp]
theorem units.measurable_const_smul_iff {α : Type u_1} [measurable_space α] {M : Type u_2} {β : Type u_3} [measurable_space M] [measurable_space β] [monoid M] [mul_action M β] [has_measurable_smul M β] {f : α → β} (u : units M) :
measurable (λ (x : α), u f x) measurable f
@[simp]
theorem units.ae_measurable_const_smul_iff {α : Type u_1} [measurable_space α] {M : Type u_2} {β : Type u_3} [measurable_space M] [measurable_space β] [monoid M] [mul_action M β] [has_measurable_smul M β] {f : α → β} {μ : measure_theory.measure α} (u : units M) :
ae_measurable (λ (x : α), u f x) μ ae_measurable f μ
theorem is_unit.measurable_const_smul_iff {α : Type u_1} [measurable_space α] {M : Type u_2} {β : Type u_3} [measurable_space M] [measurable_space β] [monoid M] [mul_action M β] [has_measurable_smul M β] {f : α → β} {c : M} (hc : is_unit c) :
measurable (λ (x : α), c f x) measurable f
theorem is_unit.ae_measurable_const_smul_iff {α : Type u_1} [measurable_space α] {M : Type u_2} {β : Type u_3} [measurable_space M] [measurable_space β] [monoid M] [mul_action M β] [has_measurable_smul M β] {f : α → β} {μ : measure_theory.measure α} {c : M} (hc : is_unit c) :
ae_measurable (λ (x : α), c f x) μ ae_measurable f μ
theorem measurable_const_smul_iff' {α : Type u_1} [measurable_space α] {β : Type u_3} [measurable_space β] {f : α → β} {G₀ : Type u_4} [group_with_zero G₀] [measurable_space G₀] [mul_action G₀ β] [has_measurable_smul G₀ β] {c : G₀} (hc : c 0) :
measurable (λ (x : α), c f x) measurable f
theorem ae_measurable_const_smul_iff' {α : Type u_1} [measurable_space α] {β : Type u_3} [measurable_space β] {f : α → β} {μ : measure_theory.measure α} {G₀ : Type u_4} [group_with_zero G₀] [measurable_space G₀] [mul_action G₀ β] [has_measurable_smul G₀ β] {c : G₀} (hc : c 0) :
ae_measurable (λ (x : α), c f x) μ ae_measurable f μ
theorem measurable_const_smul_iff {α : Type u_1} [measurable_space α] {β : Type u_3} [measurable_space β] {f : α → β} {G : Type u_5} [group G] [measurable_space G] [mul_action G β] [has_measurable_smul G β] (c : G) :
measurable (λ (x : α), c f x) measurable f
theorem ae_measurable_const_smul_iff {α : Type u_1} [measurable_space α] {β : Type u_3} [measurable_space β] {f : α → β} {μ : measure_theory.measure α} {G : Type u_5} [group G] [measurable_space G] [mul_action G β] [has_measurable_smul G β] (c : G) :
ae_measurable (λ (x : α), c f x) μ ae_measurable f μ

Big operators: and #

theorem list.measurable_prod' {α : Type u_1} [measurable_space α] {M : Type u_2} [monoid M] [measurable_space M] [has_measurable_mul₂ M] (l : list (α → M)) (hl : ∀ (f : α → M), f lmeasurable f) :
theorem list.measurable_sum' {α : Type u_1} [measurable_space α] {M : Type u_2} [add_monoid M] [measurable_space M] [has_measurable_add₂ M] (l : list (α → M)) (hl : ∀ (f : α → M), f lmeasurable f) :
theorem list.ae_measurable_prod' {α : Type u_1} [measurable_space α] {M : Type u_2} [monoid M] [measurable_space M] [has_measurable_mul₂ M] {μ : measure_theory.measure α} (l : list (α → M)) (hl : ∀ (f : α → M), f lae_measurable f μ) :
theorem list.ae_measurable_sum' {α : Type u_1} [measurable_space α] {M : Type u_2} [add_monoid M] [measurable_space M] [has_measurable_add₂ M] {μ : measure_theory.measure α} (l : list (α → M)) (hl : ∀ (f : α → M), f lae_measurable f μ) :
theorem list.measurable_prod {α : Type u_1} [measurable_space α] {M : Type u_2} [monoid M] [measurable_space M] [has_measurable_mul₂ M] (l : list (α → M)) (hl : ∀ (f : α → M), f lmeasurable f) :
measurable (λ (x : α), (list.map (λ (f : α → M), f x) l).prod)
theorem list.measurable_sum {α : Type u_1} [measurable_space α] {M : Type u_2} [add_monoid M] [measurable_space M] [has_measurable_add₂ M] (l : list (α → M)) (hl : ∀ (f : α → M), f lmeasurable f) :
measurable (λ (x : α), (list.map (λ (f : α → M), f x) l).sum)
theorem list.ae_measurable_prod {α : Type u_1} [measurable_space α] {M : Type u_2} [monoid M] [measurable_space M] [has_measurable_mul₂ M] {μ : measure_theory.measure α} (l : list (α → M)) (hl : ∀ (f : α → M), f lae_measurable f μ) :
ae_measurable (λ (x : α), (list.map (λ (f : α → M), f x) l).prod) μ
theorem list.ae_measurable_sum {α : Type u_1} [measurable_space α] {M : Type u_2} [add_monoid M] [measurable_space M] [has_measurable_add₂ M] {μ : measure_theory.measure α} (l : list (α → M)) (hl : ∀ (f : α → M), f lae_measurable f μ) :
ae_measurable (λ (x : α), (list.map (λ (f : α → M), f x) l).sum) μ
theorem multiset.measurable_prod' {α : Type u_1} [measurable_space α] {M : Type u_2} [comm_monoid M] [measurable_space M] [has_measurable_mul₂ M] (l : multiset (α → M)) (hl : ∀ (f : α → M), f lmeasurable f) :
theorem multiset.measurable_sum' {α : Type u_1} [measurable_space α] {M : Type u_2} [add_comm_monoid M] [measurable_space M] [has_measurable_add₂ M] (l : multiset (α → M)) (hl : ∀ (f : α → M), f lmeasurable f) :
theorem multiset.ae_measurable_prod' {α : Type u_1} [measurable_space α] {M : Type u_2} [comm_monoid M] [measurable_space M] [has_measurable_mul₂ M] {μ : measure_theory.measure α} (l : multiset (α → M)) (hl : ∀ (f : α → M), f lae_measurable f μ) :
theorem multiset.ae_measurable_sum' {α : Type u_1} [measurable_space α] {M : Type u_2} [add_comm_monoid M] [measurable_space M] [has_measurable_add₂ M] {μ : measure_theory.measure α} (l : multiset (α → M)) (hl : ∀ (f : α → M), f lae_measurable f μ) :
theorem multiset.measurable_prod {α : Type u_1} [measurable_space α] {M : Type u_2} [comm_monoid M] [measurable_space M] [has_measurable_mul₂ M] (s : multiset (α → M)) (hs : ∀ (f : α → M), f smeasurable f) :
measurable (λ (x : α), (multiset.map (λ (f : α → M), f x) s).prod)
theorem multiset.measurable_sum {α : Type u_1} [measurable_space α] {M : Type u_2} [add_comm_monoid M] [measurable_space M] [has_measurable_add₂ M] (s : multiset (α → M)) (hs : ∀ (f : α → M), f smeasurable f) :
measurable (λ (x : α), (multiset.map (λ (f : α → M), f x) s).sum)
theorem multiset.ae_measurable_prod {α : Type u_1} [measurable_space α] {M : Type u_2} [comm_monoid M] [measurable_space M] [has_measurable_mul₂ M] {μ : measure_theory.measure α} (s : multiset (α → M)) (hs : ∀ (f : α → M), f sae_measurable f μ) :
ae_measurable (λ (x : α), (multiset.map (λ (f : α → M), f x) s).prod) μ
theorem multiset.ae_measurable_sum {α : Type u_1} [measurable_space α] {M : Type u_2} [add_comm_monoid M] [measurable_space M] [has_measurable_add₂ M] {μ : measure_theory.measure α} (s : multiset (α → M)) (hs : ∀ (f : α → M), f sae_measurable f μ) :
ae_measurable (λ (x : α), (multiset.map (λ (f : α → M), f x) s).sum) μ
theorem finset.measurable_sum' {α : Type u_1} [measurable_space α] {ι : Type u_2} {M : Type u_3} [add_comm_monoid M] [measurable_space M] [has_measurable_add₂ M] {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i smeasurable (f i)) :
measurable (∑ (i : ι) in s, f i)
theorem finset.measurable_prod' {α : Type u_1} [measurable_space α] {ι : Type u_2} {M : Type u_3} [comm_monoid M] [measurable_space M] [has_measurable_mul₂ M] {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i smeasurable (f i)) :
measurable (∏ (i : ι) in s, f i)
theorem finset.measurable_sum {α : Type u_1} [measurable_space α] {ι : Type u_2} {M : Type u_3} [add_comm_monoid M] [measurable_space M] [has_measurable_add₂ M] {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i smeasurable (f i)) :
measurable (λ (a : α), ∑ (i : ι) in s, f i a)
theorem finset.measurable_prod {α : Type u_1} [measurable_space α] {ι : Type u_2} {M : Type u_3} [comm_monoid M] [measurable_space M] [has_measurable_mul₂ M] {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i smeasurable (f i)) :
measurable (λ (a : α), ∏ (i : ι) in s, f i a)
theorem finset.ae_measurable_sum' {α : Type u_1} [measurable_space α] {ι : Type u_2} {M : Type u_3} [add_comm_monoid M] [measurable_space M] [has_measurable_add₂ M] {μ : measure_theory.measure α} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i sae_measurable (f i) μ) :
ae_measurable (∑ (i : ι) in s, f i) μ
theorem finset.ae_measurable_prod' {α : Type u_1} [measurable_space α] {ι : Type u_2} {M : Type u_3} [comm_monoid M] [measurable_space M] [has_measurable_mul₂ M] {μ : measure_theory.measure α} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i sae_measurable (f i) μ) :
ae_measurable (∏ (i : ι) in s, f i) μ
theorem finset.ae_measurable_prod {α : Type u_1} [measurable_space α] {ι : Type u_2} {M : Type u_3} [comm_monoid M] [measurable_space M] [has_measurable_mul₂ M] {f : ι → α → M} {μ : measure_theory.measure α} (s : finset ι) (hf : ∀ (i : ι), i sae_measurable (f i) μ) :
ae_measurable (λ (a : α), ∏ (i : ι) in s, f i a) μ
theorem finset.ae_measurable_sum {α : Type u_1} [measurable_space α] {ι : Type u_2} {M : Type u_3} [add_comm_monoid M] [measurable_space M] [has_measurable_add₂ M] {f : ι → α → M} {μ : measure_theory.measure α} (s : finset ι) (hf : ∀ (i : ι), i sae_measurable (f i) μ) :
ae_measurable (λ (a : α), ∑ (i : ι) in s, f i a) μ