# mathlibdocumentation

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:

• 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.

## Tags #

measurable function, arithmetic operator

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

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

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

Instances
@[instance]
def has_measurable_mul.has_measurable_pow (M : Type u_1) [monoid M]  :
Equations
theorem measurable.pow {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ γ] [ γ] {f : α → β} {g : α → γ} (hf : measurable f) (hg : measurable g) :
measurable (λ (x : α), f x ^ g x)
theorem ae_measurable.pow {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ γ] [ γ] {μ : measure_theory.measure α} {f : α → β} {g : α → γ} (hf : μ) (hg : μ) :
ae_measurable (λ (x : α), f x ^ g x) μ
theorem measurable.pow_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ γ] [ γ] {f : α → β} (hf : measurable f) (c : γ) :
measurable (λ (x : α), f x ^ c)
theorem ae_measurable.pow_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ γ] [ γ] {μ : measure_theory.measure α} {f : α → β} (hf : μ) (c : γ) :
ae_measurable (λ (x : α), f x ^ c) μ
theorem measurable.const_pow {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ γ] [ γ] {f : α → γ} (hf : measurable f) (c : β) :
measurable (λ (x : α), c ^ f x)
theorem ae_measurable.const_pow {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ γ] [ γ] {μ : measure_theory.measure α} {f : α → γ} (hf : μ) (c : β) :
ae_measurable (λ (x : α), c ^ f x) μ
@[class]
structure has_measurable_sub (G : Type u_2) [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) [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
• 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
@[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} {G : Type u_2} [has_div G] {f g : α → G} (hf : measurable f) (hg : measurable g) :
measurable (λ (a : α), f a / g a)
theorem measurable.sub {α : Type u_1} {G : Type u_2} [has_sub G] {f g : α → G} (hf : measurable f) (hg : measurable g) :
measurable (λ (a : α), f a - g a)
theorem ae_measurable.sub {α : Type u_1} {G : Type u_2} [has_sub G] {f g : α → G} {μ : measure_theory.measure α} (hf : μ) (hg : μ) :
ae_measurable (λ (a : α), f a - g a) μ
theorem ae_measurable.div {α : Type u_1} {G : Type u_2} [has_div G] {f g : α → G} {μ : measure_theory.measure α} (hf : μ) (hg : μ) :
ae_measurable (λ (a : α), f a / g a) μ
@[instance]
@[instance]
theorem measurable.const_div {α : Type u_1} {G : Type u_2} [has_div G] {f : α → G} (hf : measurable f) (c : G) :
measurable (λ (x : α), c / f x)
theorem measurable.const_sub {α : Type u_1} {G : Type u_2} [has_sub G] {f : α → G} (hf : measurable f) (c : G) :
measurable (λ (x : α), c - f x)
theorem ae_measurable.const_sub {α : Type u_1} {G : Type u_2} [has_sub G] {f : α → G} {μ : measure_theory.measure α} (hf : μ) (c : G) :
ae_measurable (λ (x : α), c - f x) μ
theorem ae_measurable.const_div {α : Type u_1} {G : Type u_2} [has_div G] {f : α → G} {μ : measure_theory.measure α} (hf : μ) (c : G) :
ae_measurable (λ (x : α), c / f x) μ
theorem measurable.sub_const {α : Type u_1} {G : Type u_2} [has_sub G] {f : α → G} (hf : measurable f) (c : G) :
measurable (λ (x : α), f x - c)
theorem measurable.div_const {α : Type u_1} {G : Type u_2} [has_div G] {f : α → G} (hf : measurable f) (c : G) :
measurable (λ (x : α), f x / c)
theorem ae_measurable.sub_const {α : Type u_1} {G : Type u_2} [has_sub G] {f : α → G} {μ : measure_theory.measure α} (hf : μ) (c : G) :
ae_measurable (λ (x : α), f x - c) μ
theorem ae_measurable.div_const {α : Type u_1} {G : Type u_2} [has_div G] {f : α → G} {μ : measure_theory.measure α} (hf : μ) (c : G) :
ae_measurable (λ (x : α), f x / c) μ
@[class]
structure has_measurable_neg (G : Type u_2) [has_neg G]  :
Prop
• measurable_neg :

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]  :
Prop
• measurable_inv :

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

Instances
@[instance]
def has_measurable_div_of_mul_inv (G : Type u_1)  :
@[instance]
def has_measurable_sub_of_add_neg (G : Type u_1)  :
theorem measurable.inv {α : Type u_1} {G : Type u_2} [has_inv G] {f : α → G} (hf : measurable f) :
measurable (λ (x : α), (f x)⁻¹)
theorem measurable.neg {α : Type u_1} {G : Type u_2} [has_neg G] {f : α → G} (hf : measurable f) :
measurable (λ (x : α), -f x)
theorem ae_measurable.neg {α : Type u_1} {G : Type u_2} [has_neg G] {f : α → G} {μ : measure_theory.measure α} (hf : μ) :
ae_measurable (λ (x : α), -f x) μ
theorem ae_measurable.inv {α : Type u_1} {G : Type u_2} [has_inv G] {f : α → G} {μ : measure_theory.measure α} (hf : μ) :
ae_measurable (λ (x : α), (f x)⁻¹) μ
@[simp]
theorem measurable_inv_iff {α : Type u_1} {G : Type u_2} [group G] {f : α → G} :
measurable (λ (x : α), (f x)⁻¹)
@[simp]
theorem measurable_neg_iff {α : Type u_1} {G : Type u_2} [add_group G] {f : α → G} :
measurable (λ (x : α), -f x)
@[simp]
theorem ae_measurable_inv_iff {α : Type u_1} {G : Type u_2} [group G] {f : α → G} {μ : measure_theory.measure α} :
ae_measurable (λ (x : α), (f x)⁻¹) μ
@[simp]
theorem ae_measurable_neg_iff {α : Type u_1} {G : Type u_2} [add_group G] {f : α → G} {μ : measure_theory.measure α} :
ae_measurable (λ (x : α), -f x) μ
@[simp]
theorem measurable_inv_iff' {α : Type u_1} {G₀ : Type u_2} [group_with_zero G₀] [measurable_space G₀] {f : α → G₀} :
measurable (λ (x : α), (f x)⁻¹)
@[simp]
theorem ae_measurable_inv_iff' {α : Type u_1} {G₀ : Type u_2} [group_with_zero G₀] [measurable_space G₀] {f : α → G₀} {μ : measure_theory.measure α} :
ae_measurable (λ (x : α), (f x)⁻¹) μ
@[instance]
def has_measurable_gpow (G : Type u)  :
Equations
@[instance]
def has_measurable_div₂_of_mul_inv (G : Type u_1)  :
@[instance]
def has_measurable_div₂_of_add_neg (G : Type u_1)  :
@[class]
structure has_measurable_smul (M : Type u_2) (α : Type u_3) [ α]  :
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
@[class]
structure has_measurable_smul₂ (M : Type u_2) (α : Type u_3) [ α]  :
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
@[instance]
def has_measurable_smul_of_mul (M : Type u_1) [monoid M]  :
@[instance]
def has_measurable_smul₂_of_mul (M : Type u_1) [monoid M]  :
theorem measurable.smul {α : Type u_1} {M : Type u_2} {β : Type u_3} [ β] [ β] {f : α → M} {g : α → β} (hf : measurable f) (hg : measurable g) :
measurable (λ (x : α), f x g x)
theorem ae_measurable.smul {α : Type u_1} {M : Type u_2} {β : Type u_3} [ β] [ β] {f : α → M} {g : α → β} {μ : measure_theory.measure α} (hf : μ) (hg : μ) :
ae_measurable (λ (x : α), f x g x) μ
@[instance]
def has_measurable_smul₂.to_has_measurable_smul {M : Type u_2} {β : Type u_3} [ β] [ β] :
theorem measurable.smul_const {α : Type u_1} {M : Type u_2} {β : Type u_3} [ β] [ β] {f : α → M} (hf : measurable f) (y : β) :
measurable (λ (x : α), f x y)
theorem ae_measurable.smul_const {α : Type u_1} {M : Type u_2} {β : Type u_3} [ β] [ β] {μ : measure_theory.measure α} {f : α → M} (hf : μ) (y : β) :
ae_measurable (λ (x : α), f x y) μ
theorem measurable.const_smul' {α : Type u_1} {M : Type u_2} {β : Type u_3} [ β] [ β] {f : α → β} (hf : measurable f) (c : M) :
measurable (λ (x : α), c f x)
theorem measurable.const_smul {α : Type u_1} {M : Type u_2} {β : Type u_3} [ β] [ β] {f : α → β} (hf : measurable f) (c : M) :
theorem ae_measurable.const_smul' {α : Type u_1} {M : Type u_2} {β : Type u_3} [ β] [ β] {μ : measure_theory.measure α} {f : α → β} (hf : μ) (c : M) :
ae_measurable (λ (x : α), c f x) μ
theorem ae_measurable.const_smul {α : Type u_1} {M : Type u_2} {β : Type u_3} [ β] [ β] {μ : measure_theory.measure α} {f : α → β} (hf : μ) (c : M) :
@[simp]
theorem units.measurable_const_smul_iff {α : Type u_1} {M : Type u_2} {β : Type u_3} [monoid M] [ β] [ β] {f : α → β} (u : units M) :
measurable (λ (x : α), u f x)
@[simp]
theorem units.ae_measurable_const_smul_iff {α : Type u_1} {M : Type u_2} {β : Type u_3} [monoid M] [ β] [ β] {f : α → β} {μ : measure_theory.measure α} (u : units M) :
ae_measurable (λ (x : α), u f x) μ
theorem is_unit.measurable_const_smul_iff {α : Type u_1} {M : Type u_2} {β : Type u_3} [monoid M] [ β] [ β] {f : α → β} {c : M} (hc : is_unit c) :
measurable (λ (x : α), c f x)
theorem is_unit.ae_measurable_const_smul_iff {α : Type u_1} {M : 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_1} {β : Type u_3} {f : α → β} {G₀ : Type u_4} [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_1} {β : Type u_3} {f : α → β} {μ : measure_theory.measure α} {G₀ : Type u_4} [group_with_zero G₀] [measurable_space G₀] [ β] [ β] {c : G₀} (hc : c 0) :
ae_measurable (λ (x : α), c f x) μ
theorem measurable_const_smul_iff {α : Type u_1} {β : Type u_3} {f : α → β} {G : Type u_5} [group G] [ β] [ β] (c : G) :
measurable (λ (x : α), c f x)
theorem ae_measurable_const_smul_iff {α : Type u_1} {β : Type u_3} {f : α → β} {μ : measure_theory.measure α} {G : Type u_5} [group G] [ β] [ β] (c : G) :
ae_measurable (λ (x : α), c f x) μ

### Big operators: ∏ and ∑#

theorem list.measurable_prod' {α : Type u_1} {M : Type u_2} [monoid M] (l : list (α → M)) (hl : ∀ (f : α → M), f l) :
theorem list.measurable_sum' {α : Type u_1} {M : Type u_2} [add_monoid M] (l : list (α → M)) (hl : ∀ (f : α → M), f l) :
theorem list.ae_measurable_prod' {α : Type u_1} {M : Type u_2} [monoid M] {μ : measure_theory.measure α} (l : list (α → M)) (hl : ∀ (f : α → M), f l) :
theorem list.ae_measurable_sum' {α : Type u_1} {M : Type u_2} [add_monoid M] {μ : measure_theory.measure α} (l : list (α → M)) (hl : ∀ (f : α → M), f l) :
μ
theorem list.measurable_prod {α : Type u_1} {M : Type u_2} [monoid M] (l : list (α → M)) (hl : ∀ (f : α → M), f l) :
measurable (λ (x : α), (list.map (λ (f : α → M), f x) l).prod)
theorem list.measurable_sum {α : Type u_1} {M : Type u_2} [add_monoid M] (l : list (α → M)) (hl : ∀ (f : α → M), f l) :
measurable (λ (x : α), (list.map (λ (f : α → M), f x) l).sum)
theorem list.ae_measurable_prod {α : Type u_1} {M : Type u_2} [monoid M] {μ : measure_theory.measure α} (l : list (α → M)) (hl : ∀ (f : α → M), f l) :
ae_measurable (λ (x : α), (list.map (λ (f : α → M), f x) l).prod) μ
theorem list.ae_measurable_sum {α : Type u_1} {M : Type u_2} [add_monoid M] {μ : measure_theory.measure α} (l : list (α → M)) (hl : ∀ (f : α → M), f l) :
ae_measurable (λ (x : α), (list.map (λ (f : α → M), f x) l).sum) μ
theorem multiset.measurable_prod' {α : Type u_1} {M : Type u_2} [comm_monoid M] (l : multiset (α → M)) (hl : ∀ (f : α → M), f l) :
theorem multiset.measurable_sum' {α : Type u_1} {M : Type u_2} (l : multiset (α → M)) (hl : ∀ (f : α → M), f l) :
theorem multiset.ae_measurable_prod' {α : Type u_1} {M : Type u_2} [comm_monoid M] {μ : measure_theory.measure α} (l : multiset (α → M)) (hl : ∀ (f : α → M), f l) :
theorem multiset.ae_measurable_sum' {α : Type u_1} {M : Type u_2} {μ : measure_theory.measure α} (l : multiset (α → M)) (hl : ∀ (f : α → M), f l) :
μ
theorem multiset.measurable_prod {α : Type u_1} {M : Type u_2} [comm_monoid M] (s : multiset (α → M)) (hs : ∀ (f : α → M), f s) :
measurable (λ (x : α), (multiset.map (λ (f : α → M), f x) s).prod)
theorem multiset.measurable_sum {α : Type u_1} {M : Type u_2} (s : multiset (α → M)) (hs : ∀ (f : α → M), f s) :
measurable (λ (x : α), (multiset.map (λ (f : α → M), f x) s).sum)
theorem multiset.ae_measurable_prod {α : Type u_1} {M : Type u_2} [comm_monoid M] {μ : measure_theory.measure α} (s : multiset (α → M)) (hs : ∀ (f : α → M), f s) :
ae_measurable (λ (x : α), (multiset.map (λ (f : α → M), f x) s).prod) μ
theorem multiset.ae_measurable_sum {α : Type u_1} {M : Type u_2} {μ : measure_theory.measure α} (s : multiset (α → M)) (hs : ∀ (f : α → M), f s) :
ae_measurable (λ (x : α), (multiset.map (λ (f : α → M), f x) s).sum) μ
theorem finset.measurable_sum' {α : Type u_1} {ι : Type u_2} {M : Type u_3} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i smeasurable (f i)) :
measurable (∑ (i : ι) in s, f i)
theorem finset.measurable_prod' {α : Type u_1} {ι : Type u_2} {M : Type u_3} [comm_monoid M] {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i smeasurable (f i)) :
measurable (∏ (i : ι) in s, f i)
theorem finset.measurable_sum {α : Type u_1} {ι : Type u_2} {M : Type u_3} {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} {ι : Type u_2} {M : Type u_3} [comm_monoid 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} {ι : Type u_2} {M : Type u_3} {μ : 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} {ι : Type u_2} {M : Type u_3} [comm_monoid 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} {ι : Type u_2} {M : Type u_3} [comm_monoid 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} {ι : Type u_2} {M : Type u_3} {f : ι → α → M} {μ : measure_theory.measure α} (s : finset ι) (hf : ∀ (i : ι), i sae_measurable (f i) μ) :
ae_measurable (λ (a : α), ∑ (i : ι) in s, f i a) μ