# mathlibdocumentation

measure_theory.group.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:

• has_measurable_mul says that both left and right multiplication are measurable;
• has_measurable_mul₂ says that λ p : α × α, p.1 * p.2 is measurable,

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.

## Implementation notes #

For the heuristics of @[to_additive] it is important that the type with a multiplication (or another multiplicative operations) is the first (implicit) argument of all declarations.

## Tags #

measurable function, arithmetic operator

## Todo #

• Uniformize the treatment of pow and smul.
• Use @[to_additive] to send has_measurable_pow to has_measurable_smul₂.
• This might require changing the definition (swapping the arguments in the function that is in the conclusion of measurable_smul.)

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

@[class]
Prop
• measurable_const_add : ∀ (c : M),
• measurable_add_const : ∀ (c : M), measurable (λ (_x : M), _x + c)

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 of this typeclass
@[class]
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 of this typeclass
@[class]
structure has_measurable_mul (M : Type u_1) [has_mul M] :
Prop
• measurable_const_mul : ∀ (c : M),
• measurable_mul_const : ∀ (c : M), measurable (λ (_x : M), _x * c)

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 of this typeclass
@[class]
structure has_measurable_mul₂ (M : Type u_1) [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 of this typeclass
@[measurability]
theorem measurable.const_add {M : Type u_1} {α : Type u_2} [has_add M] {m : measurable_space α} {f : α → M} (hf : measurable f) (c : M) :
measurable (λ (x : α), c + f x)
@[measurability]
theorem measurable.const_mul {M : Type u_1} {α : Type u_2} [has_mul M] {m : measurable_space α} {f : α → M} (hf : measurable f) (c : M) :
measurable (λ (x : α), c * f x)
@[measurability]
theorem ae_measurable.const_mul {M : Type u_1} {α : Type u_2} [has_mul M] {m : measurable_space α} {f : α → M} {μ : measure_theory.measure α} (hf : μ) (c : M) :
ae_measurable (λ (x : α), c * f x) μ
@[measurability]
theorem ae_measurable.const_add {M : Type u_1} {α : Type u_2} [has_add M] {m : measurable_space α} {f : α → M} {μ : measure_theory.measure α} (hf : μ) (c : M) :
ae_measurable (λ (x : α), c + f x) μ
@[measurability]
theorem measurable.add_const {M : Type u_1} {α : Type u_2} [has_add M] {m : measurable_space α} {f : α → M} (hf : measurable f) (c : M) :
measurable (λ (x : α), f x + c)
@[measurability]
theorem measurable.mul_const {M : Type u_1} {α : Type u_2} [has_mul M] {m : measurable_space α} {f : α → M} (hf : measurable f) (c : M) :
measurable (λ (x : α), f x * c)
@[measurability]
theorem ae_measurable.mul_const {M : Type u_1} {α : Type u_2} [has_mul M] {m : measurable_space α} {f : α → M} {μ : measure_theory.measure α} (hf : μ) (c : M) :
ae_measurable (λ (x : α), f x * c) μ
@[measurability]
theorem ae_measurable.add_const {M : Type u_1} {α : Type u_2} [has_add M] {m : measurable_space α} {f : α → M} {μ : measure_theory.measure α} (hf : μ) (c : M) :
ae_measurable (λ (x : α), f x + c) μ
@[measurability]
theorem measurable.add' {M : Type u_1} {α : Type u_2} [has_add M] {m : measurable_space α} {f g : α → M} (hf : measurable f) (hg : measurable g) :
@[measurability]
theorem measurable.mul' {M : Type u_1} {α : Type u_2} [has_mul M] {m : measurable_space α} {f g : α → M} (hf : measurable f) (hg : measurable g) :
@[measurability]
theorem measurable.add {M : Type u_1} {α : Type u_2} [has_add M] {m : measurable_space α} {f g : α → M} (hf : measurable f) (hg : measurable g) :
measurable (λ (a : α), f a + g a)
@[measurability]
theorem measurable.mul {M : Type u_1} {α : Type u_2} [has_mul M] {m : measurable_space α} {f g : α → M} (hf : measurable f) (hg : measurable g) :
measurable (λ (a : α), f a * g a)
@[measurability]
theorem ae_measurable.mul' {M : Type u_1} {α : Type u_2} [has_mul M] {m : measurable_space α} {f g : α → M} {μ : measure_theory.measure α} (hf : μ) (hg : μ) :
ae_measurable (f * g) μ
@[measurability]
theorem ae_measurable.add' {M : Type u_1} {α : Type u_2} [has_add M] {m : measurable_space α} {f g : α → M} {μ : measure_theory.measure α} (hf : μ) (hg : μ) :
ae_measurable (f + g) μ
@[measurability]
theorem ae_measurable.add {M : Type u_1} {α : Type u_2} [has_add M] {m : measurable_space α} {f g : α → M} {μ : measure_theory.measure α} (hf : μ) (hg : μ) :
ae_measurable (λ (a : α), f a + g a) μ
@[measurability]
theorem ae_measurable.mul {M : Type u_1} {α : Type u_2} [has_mul M] {m : measurable_space α} {f g : α → M} {μ : measure_theory.measure α} (hf : μ) (hg : μ) :
ae_measurable (λ (a : α), f a * g a) μ
@[protected, instance]
@[protected, instance]
@[protected, instance]
def pi.has_measurable_mul {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_mul (α i)] [Π (i : ι), measurable_space (α i)] [∀ (i : ι), has_measurable_mul (α i)] :
has_measurable_mul (Π (i : ι), α i)
@[protected, instance]
def pi.has_measurable_add {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_add (α i)] [Π (i : ι), measurable_space (α i)] [∀ (i : ι), has_measurable_add (α i)] :
has_measurable_add (Π (i : ι), α i)
@[protected, instance]
def pi.has_measurable_add₂ {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_add (α i)] [Π (i : ι), measurable_space (α i)] [∀ (i : ι), has_measurable_add₂ (α i)] :
has_measurable_add₂ (Π (i : ι), α i)
@[protected, instance]
def pi.has_measurable_mul₂ {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_mul (α i)] [Π (i : ι), measurable_space (α i)] [∀ (i : ι), has_measurable_mul₂ (α i)] :
has_measurable_mul₂ (Π (i : ι), α i)
theorem measurable_div_const' {G : Type u_1} (g : G) :
measurable (λ (h : G), h / g)

A version of measurable_div_const that assumes has_measurable_mul instead of has_measurable_div. This can be nice to avoid unnecessary type-class assumptions.

theorem measurable_sub_const' {G : Type u_1} (g : G) :
measurable (λ (h : G), h - g)

A version of measurable_sub_const that assumes has_measurable_add instead of has_measurable_sub. This can be nice to avoid unnecessary type-class assumptions.

@[class]
structure has_measurable_pow (β : Type u_1) (γ : Type u_2) [ γ] :
Type

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

Instances of this typeclass
Instances of other typeclasses for has_measurable_pow
• has_measurable_pow.has_sizeof_inst
@[protected, instance]
def monoid.has_measurable_pow (M : Type u_1) [monoid M]  :

monoid.has_pow is measurable.

Equations
@[measurability]
theorem measurable.pow {β : Type u_1} {γ : Type u_2} {α : Type u_3} [ γ] [ γ] {m : measurable_space α} {f : α → β} {g : α → γ} (hf : measurable f) (hg : measurable g) :
measurable (λ (x : α), f x ^ g x)
@[measurability]
theorem ae_measurable.pow {β : Type u_1} {γ : Type u_2} {α : Type u_3} [ γ] [ γ] {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} {g : α → γ} (hf : μ) (hg : μ) :
ae_measurable (λ (x : α), f x ^ g x) μ
@[measurability]
theorem measurable.pow_const {β : Type u_1} {γ : Type u_2} {α : Type u_3} [ γ] [ γ] {m : measurable_space α} {f : α → β} (hf : measurable f) (c : γ) :
measurable (λ (x : α), f x ^ c)
@[measurability]
theorem ae_measurable.pow_const {β : Type u_1} {γ : Type u_2} {α : Type u_3} [ γ] [ γ] {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} (hf : μ) (c : γ) :
ae_measurable (λ (x : α), f x ^ c) μ
@[measurability]
theorem measurable.const_pow {β : Type u_1} {γ : Type u_2} {α : Type u_3} [ γ] [ γ] {m : measurable_space α} {g : α → γ} (hg : measurable g) (c : β) :
measurable (λ (x : α), c ^ g x)
@[measurability]
theorem ae_measurable.const_pow {β : Type u_1} {γ : Type u_2} {α : Type u_3} [ γ] [ γ] {m : measurable_space α} {μ : measure_theory.measure α} {g : α → γ} (hg : μ) (c : β) :
ae_measurable (λ (x : α), c ^ g x) μ
@[class]
structure has_measurable_sub (G : Type u_1) [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 of this typeclass
@[class]
structure has_measurable_sub₂ (G : Type u_1) [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 of this typeclass
@[class]
structure has_measurable_div (G₀ : Type u_1) [measurable_space G₀] [has_div G₀] :
Prop
• measurable_const_div : ∀ (c : G₀),
• measurable_div_const : ∀ (c : G₀), measurable (λ (_x : G₀), _x / c)

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 of this typeclass
@[class]
structure has_measurable_div₂ (G₀ : Type u_1) [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 of this typeclass
@[measurability]
theorem measurable.const_div {G : Type u_1} {α : Type u_2} [has_div G] {m : measurable_space α} {f : α → G} (hf : measurable f) (c : G) :
measurable (λ (x : α), c / f x)
@[measurability]
theorem measurable.const_sub {G : Type u_1} {α : Type u_2} [has_sub G] {m : measurable_space α} {f : α → G} (hf : measurable f) (c : G) :
measurable (λ (x : α), c - f x)
@[measurability]
theorem ae_measurable.const_sub {G : Type u_1} {α : Type u_2} [has_sub G] {m : measurable_space α} {f : α → G} {μ : measure_theory.measure α} (hf : μ) (c : G) :
ae_measurable (λ (x : α), c - f x) μ
@[measurability]
theorem ae_measurable.const_div {G : Type u_1} {α : Type u_2} [has_div G] {m : measurable_space α} {f : α → G} {μ : measure_theory.measure α} (hf : μ) (c : G) :
ae_measurable (λ (x : α), c / f x) μ
@[measurability]
theorem measurable.sub_const {G : Type u_1} {α : Type u_2} [has_sub G] {m : measurable_space α} {f : α → G} (hf : measurable f) (c : G) :
measurable (λ (x : α), f x - c)
@[measurability]
theorem measurable.div_const {G : Type u_1} {α : Type u_2} [has_div G] {m : measurable_space α} {f : α → G} (hf : measurable f) (c : G) :
measurable (λ (x : α), f x / c)
@[measurability]
theorem ae_measurable.sub_const {G : Type u_1} {α : Type u_2} [has_sub G] {m : measurable_space α} {f : α → G} {μ : measure_theory.measure α} (hf : μ) (c : G) :
ae_measurable (λ (x : α), f x - c) μ
@[measurability]
theorem ae_measurable.div_const {G : Type u_1} {α : Type u_2} [has_div G] {m : measurable_space α} {f : α → G} {μ : measure_theory.measure α} (hf : μ) (c : G) :
ae_measurable (λ (x : α), f x / c) μ
@[measurability]
theorem measurable.sub' {G : Type u_1} {α : Type u_2} [has_sub G] {m : measurable_space α} {f g : α → G} (hf : measurable f) (hg : measurable g) :
@[measurability]
theorem measurable.div' {G : Type u_1} {α : Type u_2} [has_div G] {m : measurable_space α} {f g : α → G} (hf : measurable f) (hg : measurable g) :
@[measurability]
theorem measurable.div {G : Type u_1} {α : Type u_2} [has_div G] {m : measurable_space α} {f g : α → G} (hf : measurable f) (hg : measurable g) :
measurable (λ (a : α), f a / g a)
@[measurability]
theorem measurable.sub {G : Type u_1} {α : Type u_2} [has_sub G] {m : measurable_space α} {f g : α → G} (hf : measurable f) (hg : measurable g) :
measurable (λ (a : α), f a - g a)
@[measurability]
theorem ae_measurable.div' {G : Type u_1} {α : Type u_2} [has_div G] {m : measurable_space α} {f g : α → G} {μ : measure_theory.measure α} (hf : μ) (hg : μ) :
ae_measurable (f / g) μ
@[measurability]
theorem ae_measurable.sub' {G : Type u_1} {α : Type u_2} [has_sub G] {m : measurable_space α} {f g : α → G} {μ : measure_theory.measure α} (hf : μ) (hg : μ) :
ae_measurable (f - g) μ
@[measurability]
theorem ae_measurable.sub {G : Type u_1} {α : Type u_2} [has_sub G] {m : measurable_space α} {f g : α → G} {μ : measure_theory.measure α} (hf : μ) (hg : μ) :
ae_measurable (λ (a : α), f a - g a) μ
@[measurability]
theorem ae_measurable.div {G : Type u_1} {α : Type u_2} [has_div G] {m : measurable_space α} {f g : α → G} {μ : measure_theory.measure α} (hf : μ) (hg : μ) :
ae_measurable (λ (a : α), f a / g a) μ
@[protected, instance]
@[protected, instance]
@[protected, instance]
def pi.has_measurable_sub {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_sub (α i)] [Π (i : ι), measurable_space (α i)] [∀ (i : ι), has_measurable_sub (α i)] :
has_measurable_sub (Π (i : ι), α i)
@[protected, instance]
def pi.has_measurable_div {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_div (α i)] [Π (i : ι), measurable_space (α i)] [∀ (i : ι), has_measurable_div (α i)] :
has_measurable_div (Π (i : ι), α i)
@[protected, instance]
def pi.has_measurable_sub₂ {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_sub (α i)] [Π (i : ι), measurable_space (α i)] [∀ (i : ι), has_measurable_sub₂ (α i)] :
has_measurable_sub₂ (Π (i : ι), α i)
@[protected, instance]
def pi.has_measurable_div₂ {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_div (α i)] [Π (i : ι), measurable_space (α i)] [∀ (i : ι), has_measurable_div₂ (α i)] :
has_measurable_div₂ (Π (i : ι), α i)
@[measurability]
theorem measurable_set_eq_fun {α : Type u_2} {m : measurable_space α} {E : Type u_1} [add_group E] {f g : α → E} (hf : measurable f) (hg : measurable g) :
measurable_set {x : α | f x = g x}
theorem measurable_set_eq_fun_of_encodable {α : Type u_2} {m : measurable_space α} {E : Type u_1} [encodable E] {f g : α → E} (hf : measurable f) (hg : measurable g) :
measurable_set {x : α | f x = g x}
theorem ae_eq_trim_of_measurable {α : Type u_1} {E : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} [add_group E] (hm : m m0) {f g : α → E} (hf : measurable f) (hg : measurable g) (hfg : f =ᵐ[μ] g) :
f =ᵐ[μ.trim hm] g
@[class]
structure has_measurable_neg (G : Type u_1) [has_neg G]  :
Prop
• measurable_neg :

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

Instances of this typeclass
@[class]
structure has_measurable_inv (G : Type u_1) [has_inv G]  :
Prop
• measurable_inv :

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

Instances of this typeclass
@[protected, instance]
def has_measurable_div_of_mul_inv (G : Type u_1)  :
@[protected, instance]
def has_measurable_sub_of_add_neg (G : Type u_1)  :
@[measurability]
theorem measurable.inv {G : Type u_1} {α : Type u_2} [has_inv G] {m : measurable_space α} {f : α → G} (hf : measurable f) :
measurable (λ (x : α), (f x)⁻¹)
@[measurability]
theorem measurable.neg {G : Type u_1} {α : Type u_2} [has_neg G] {m : measurable_space α} {f : α → G} (hf : measurable f) :
measurable (λ (x : α), -f x)
@[measurability]
theorem ae_measurable.neg {G : Type u_1} {α : Type u_2} [has_neg G] {m : measurable_space α} {f : α → G} {μ : measure_theory.measure α} (hf : μ) :
ae_measurable (λ (x : α), -f x) μ
@[measurability]
theorem ae_measurable.inv {G : Type u_1} {α : Type u_2} [has_inv G] {m : measurable_space α} {f : α → G} {μ : measure_theory.measure α} (hf : μ) :
ae_measurable (λ (x : α), (f x)⁻¹) μ
@[simp]
theorem measurable_inv_iff {α : Type u_2} {m : measurable_space α} {G : Type u_1} [group G] {f : α → G} :
measurable (λ (x : α), (f x)⁻¹)
@[simp]
theorem measurable_neg_iff {α : Type u_2} {m : measurable_space α} {G : Type u_1} [add_group G] {f : α → G} :
measurable (λ (x : α), -f x)
@[simp]
theorem ae_measurable_inv_iff {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {G : Type u_1} [group G] {f : α → G} :
ae_measurable (λ (x : α), (f x)⁻¹) μ
@[simp]
theorem ae_measurable_neg_iff {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {G : Type u_1} [add_group G] {f : α → G} :
ae_measurable (λ (x : α), -f x) μ
@[simp]
theorem measurable_inv_iff₀ {α : Type u_2} {m : measurable_space α} {G₀ : Type u_1} [group_with_zero G₀] [measurable_space G₀] {f : α → G₀} :
measurable (λ (x : α), (f x)⁻¹)
@[simp]
theorem ae_measurable_inv_iff₀ {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {G₀ : Type u_1} [group_with_zero G₀] [measurable_space G₀] {f : α → G₀} :
ae_measurable (λ (x : α), (f x)⁻¹) μ
@[protected, instance]
def pi.has_measurable_inv {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_inv (α i)] [Π (i : ι), measurable_space (α i)] [∀ (i : ι), has_measurable_inv (α i)] :
has_measurable_inv (Π (i : ι), α i)
@[protected, instance]
def pi.has_measurable_neg {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_neg (α i)] [Π (i : ι), measurable_space (α i)] [∀ (i : ι), has_measurable_neg (α i)] :
has_measurable_neg (Π (i : ι), α i)
theorem measurable_set.inv {G : Type u_1} [has_inv G] {s : set G} (hs : measurable_set s) :
theorem measurable_set.neg {G : Type u_1} [has_neg G] {s : set G} (hs : measurable_set s) :
@[protected, instance]
def div_inv_monoid.has_measurable_zpow (G : Type u)  :

div_inv_monoid.has_pow is measurable.

Equations
@[protected, instance]
def has_measurable_div₂_of_mul_inv (G : Type u_1)  :
@[protected, instance]
def has_measurable_div₂_of_add_neg (G : Type u_1)  :
@[class]
structure has_measurable_vadd (M : Type u_1) (α : Type u_2) [ α]  :
Prop
• measurable_const_vadd : ∀ (c : M),
• measurable_vadd_const : ∀ (x : α), measurable (λ (c : M), c +ᵥ x)

We say that the action of M on α has_measurable_vadd 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 of this typeclass
@[class]
structure has_measurable_smul (M : Type u_1) (α : Type u_2) [ α]  :
Prop
• measurable_const_smul : ∀ (c : M),
• measurable_smul_const : ∀ (x : α), measurable (λ (c : M), c x)

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 of this typeclass
@[class]
structure has_measurable_vadd₂ (M : Type u_1) (α : Type u_2) [ α]  :
Prop

We say that the action of M on α has_measurable_vadd₂ if the map (c, x) ↦ c +ᵥ x is a measurable function.

Instances of this typeclass
@[class]
structure has_measurable_smul₂ (M : Type u_1) (α : Type u_2) [ α]  :
Prop
• measurable_smul :

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

Instances of this typeclass
@[protected, instance]
@[protected, instance]
def has_measurable_smul_of_mul (M : Type u_1) [has_mul M]  :
@[protected, instance]
def has_measurable_smul₂_of_mul (M : Type u_1) [has_mul M]  :
@[protected, instance]
@[protected, instance]
def submonoid.has_measurable_smul {M : Type u_1} {α : Type u_2} [monoid M] [ α] [ α] (s : submonoid M) :
@[protected, instance]
@[protected, instance]
def subgroup.has_measurable_smul {G : Type u_1} {α : Type u_2} [group G] [ α] [ α] (s : subgroup G) :
@[protected, instance]
@[measurability]
theorem measurable.smul {M : Type u_1} {β : Type u_2} {α : Type u_3} [ β] {m : measurable_space α} {f : α → M} {g : α → β} [ β] (hf : measurable f) (hg : measurable g) :
measurable (λ (x : α), f x g x)
@[measurability]
theorem measurable.vadd {M : Type u_1} {β : Type u_2} {α : Type u_3} [ β] {m : measurable_space α} {f : α → M} {g : α → β} [ β] (hf : measurable f) (hg : measurable g) :
measurable (λ (x : α), f x +ᵥ g x)
@[measurability]
theorem ae_measurable.vadd {M : Type u_1} {β : Type u_2} {α : Type u_3} [ β] {m : measurable_space α} {f : α → M} {g : α → β} [ β] {μ : measure_theory.measure α} (hf : μ) (hg : μ) :
ae_measurable (λ (x : α), f x +ᵥ g x) μ
@[measurability]
theorem ae_measurable.smul {M : Type u_1} {β : Type u_2} {α : Type u_3} [ β] {m : measurable_space α} {f : α → M} {g : α → β} [ β] {μ : measure_theory.measure α} (hf : μ) (hg : μ) :
ae_measurable (λ (x : α), f x g x) μ
@[protected, instance]
def has_measurable_smul₂.to_has_measurable_smul {M : Type u_1} {β : Type u_2} [ β] [ β] :
@[protected, instance]
def has_measurable_vadd₂.to_has_measurable_vadd {M : Type u_1} {β : Type u_2} [ β] [ β] :
@[measurability]
theorem measurable.vadd_const {M : Type u_1} {β : Type u_2} {α : Type u_3} [ β] {m : measurable_space α} {f : α → M} [ β] (hf : measurable f) (y : β) :
measurable (λ (x : α), f x +ᵥ y)
@[measurability]
theorem measurable.smul_const {M : Type u_1} {β : Type u_2} {α : Type u_3} [ β] {m : measurable_space α} {f : α → M} [ β] (hf : measurable f) (y : β) :
measurable (λ (x : α), f x y)
@[measurability]
theorem ae_measurable.vadd_const {M : Type u_1} {β : Type u_2} {α : Type u_3} [ β] {m : measurable_space α} {f : α → M} [ β] {μ : measure_theory.measure α} (hf : μ) (y : β) :
ae_measurable (λ (x : α), f x +ᵥ y) μ
@[measurability]
theorem ae_measurable.smul_const {M : Type u_1} {β : Type u_2} {α : Type u_3} [ β] {m : measurable_space α} {f : α → M} [ β] {μ : measure_theory.measure α} (hf : μ) (y : β) :
ae_measurable (λ (x : α), f x y) μ
@[measurability]
theorem measurable.const_vadd' {M : Type u_1} {β : Type u_2} {α : Type u_3} [ β] {m : measurable_space α} {g : α → β} [ β] (hg : measurable g) (c : M) :
measurable (λ (x : α), c +ᵥ g x)
@[measurability]
theorem measurable.const_smul' {M : Type u_1} {β : Type u_2} {α : Type u_3} [ β] {m : measurable_space α} {g : α → β} [ β] (hg : measurable g) (c : M) :
measurable (λ (x : α), c g x)
@[measurability]
theorem measurable.const_vadd {M : Type u_1} {β : Type u_2} {α : Type u_3} [ β] {m : measurable_space α} {g : α → β} [ β] (hg : measurable g) (c : M) :
@[measurability]
theorem measurable.const_smul {M : Type u_1} {β : Type u_2} {α : Type u_3} [ β] {m : measurable_space α} {g : α → β} [ β] (hg : measurable g) (c : M) :
@[measurability]
theorem ae_measurable.const_smul' {M : Type u_1} {β : Type u_2} {α : Type u_3} [ β] {m : measurable_space α} {g : α → β} [ β] {μ : measure_theory.measure α} (hg : μ) (c : M) :
ae_measurable (λ (x : α), c g x) μ
@[measurability]
theorem ae_measurable.const_vadd' {M : Type u_1} {β : Type u_2} {α : Type u_3} [ β] {m : measurable_space α} {g : α → β} [ β] {μ : measure_theory.measure α} (hg : μ) (c : M) :
ae_measurable (λ (x : α), c +ᵥ g x) μ
@[measurability]
theorem ae_measurable.const_smul {M : Type u_1} {β : Type u_2} {α : Type u_3} [ β] {m : measurable_space α} {g : α → β} [ β] {μ : measure_theory.measure α} (hf : μ) (c : M) :
@[measurability]
theorem ae_measurable.const_vadd {M : Type u_1} {β : Type u_2} {α : Type u_3} [ β] {m : measurable_space α} {g : α → β} [ β] {μ : measure_theory.measure α} (hf : μ) (c : M) :
@[protected, instance]
def pi.has_measurable_smul {M : Type u_1} {ι : Type u_2} {α : ι → Type u_3} [Π (i : ι), (α i)] [Π (i : ι), measurable_space (α i)] [∀ (i : ι), (α i)] :
(Π (i : ι), α i)
@[protected, instance]
def pi.has_measurable_vadd {M : Type u_1} {ι : Type u_2} {α : ι → Type u_3} [Π (i : ι), (α i)] [Π (i : ι), measurable_space (α i)] [∀ (i : ι), (α i)] :
(Π (i : ι), α i)
@[protected, instance]

add_monoid.has_smul_nat is measurable.

@[protected, instance]

sub_neg_monoid.has_smul_int is measurable.

theorem measurable_const_vadd_iff {β : Type u_2} {α : Type u_3} {f : α → β} {G : Type u_4} [add_group G] [ β] [ β] (c : G) :
measurable (λ (x : α), c +ᵥ f x)
theorem measurable_const_smul_iff {β : Type u_2} {α : Type u_3} {f : α → β} {G : Type u_4} [group G] [ β] [ β] (c : G) :
measurable (λ (x : α), c f x)
theorem ae_measurable_const_vadd_iff {β : Type u_2} {α : Type u_3} {f : α → β} {μ : measure_theory.measure α} {G : Type u_4} [add_group G] [ β] [ β] (c : G) :
ae_measurable (λ (x : α), c +ᵥ f x) μ
theorem ae_measurable_const_smul_iff {β : Type u_2} {α : Type u_3} {f : α → β} {μ : measure_theory.measure α} {G : Type u_4} [group G] [ β] [ β] (c : G) :
ae_measurable (λ (x : α), c f x) μ
@[protected, instance]
def units.measurable_space {M : Type u_1} [monoid M] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def units.has_measurable_smul {M : Type u_1} {β : Type u_2} [monoid M] [ β] [ β] :
@[protected, instance]
def add_units.has_measurable_vadd {M : Type u_1} {β : Type u_2} [add_monoid M] [ β] [ β] :
theorem is_unit.measurable_const_smul_iff {M : Type u_1} {β : Type u_2} {α : Type u_3} [monoid M] [ β] [ β] {f : α → β} {c : M} (hc : is_unit c) :
measurable (λ (x : α), c f x)
theorem is_add_unit.measurable_const_vadd_iff {M : Type u_1} {β : Type u_2} {α : Type u_3} [add_monoid M] [ β] [ β] {f : α → β} {c : M} (hc : is_add_unit c) :
measurable (λ (x : α), c +ᵥ f x)
theorem is_add_unit.ae_measurable_const_vadd_iff {M : Type u_1} {β : Type u_2} {α : Type u_3} [add_monoid M] [ β] [ β] {f : α → β} {μ : measure_theory.measure α} {c : M} (hc : is_add_unit c) :
ae_measurable (λ (x : α), c +ᵥ f x) μ
theorem is_unit.ae_measurable_const_smul_iff {M : Type u_1} {β : Type u_2} {α : Type u_3} [monoid M] [ β] [ β] {f : α → β} {μ : measure_theory.measure α} {c : M} (hc : is_unit c) :
ae_measurable (λ (x : α), c f x) μ
theorem measurable_const_smul_iff₀ {β : Type u_2} {α : Type u_3} {f : α → β} {G₀ : Type u_5} [group_with_zero G₀] [measurable_space G₀] [ β] [ β] {c : G₀} (hc : c 0) :
measurable (λ (x : α), c f x)
theorem ae_measurable_const_smul_iff₀ {β : Type u_2} {α : Type u_3} {f : α → β} {μ : measure_theory.measure α} {G₀ : Type u_5} [group_with_zero G₀] [measurable_space G₀] [ β] [ β] {c : G₀} (hc : c 0) :
ae_measurable (λ (x : α), c f x) μ

### Opposite monoid #

@[protected, instance]
def add_opposite.measurable_space {α : Type u_1} [h : measurable_space α] :
Equations
@[protected, instance]
def mul_opposite.measurable_space {α : Type u_1} [h : measurable_space α] :
Equations
theorem measurable_add_op {α : Type u_1}  :
theorem measurable_mul_op {α : Type u_1}  :
theorem measurable_add_unop {α : Type u_1}  :
theorem measurable_mul_unop {α : Type u_1}  :
@[protected, instance]
def mul_opposite.has_measurable_mul {M : Type u_1} [has_mul M]  :
@[protected, instance]
@[protected, instance]
@[protected, instance]
def mul_opposite.has_measurable_mul₂ {M : Type u_1} [has_mul M]  :
@[protected, instance]
def has_measurable_smul.op {M : Type u_1} {α : Type u_2} [ α] [ α] [ α] [ α] :

If a scalar is central, then its right action is measurable when its left action is.

@[protected, instance]
def has_measurable_smul₂.op {M : Type u_1} {α : Type u_2} [ α] [ α] [ α] [ α] :

If a scalar is central, then its right action is measurable when its left action is.

@[protected, instance]
@[protected, instance]
def has_measurable_smul_opposite_of_mul {M : Type u_1} [has_mul M]  :
@[protected, instance]
@[protected, instance]
def has_measurable_smul₂_opposite_of_mul {M : Type u_1} [has_mul M]  :

### Big operators: ∏ and ∑#

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