mathlib documentation

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:

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 #

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

@[class]
structure has_measurable_add (M : Type u_1) [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 of this typeclass
@[class]
structure has_measurable_add₂ (M : Type u_1) [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 of this typeclass
@[class]
structure has_measurable_mul (M : Type u_1) [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 of this typeclass
@[class]
structure has_measurable_mul₂ (M : Type u_1) [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 of this typeclass
@[measurability]
theorem measurable.const_add {M : Type u_1} {α : Type u_2} [measurable_space M] [has_add M] {m : measurable_space α} {f : α → M} [has_measurable_add M] (hf : measurable f) (c : M) :
measurable (λ (x : α), c + f x)
@[measurability]
theorem measurable.const_mul {M : Type u_1} {α : Type u_2} [measurable_space M] [has_mul M] {m : measurable_space α} {f : α → M} [has_measurable_mul M] (hf : measurable f) (c : M) :
measurable (λ (x : α), c * f x)
@[measurability]
theorem ae_measurable.const_mul {M : Type u_1} {α : Type u_2} [measurable_space M] [has_mul M] {m : measurable_space α} {f : α → M} {μ : measure_theory.measure α} [has_measurable_mul M] (hf : ae_measurable f μ) (c : M) :
ae_measurable (λ (x : α), c * f x) μ
@[measurability]
theorem ae_measurable.const_add {M : Type u_1} {α : Type u_2} [measurable_space M] [has_add M] {m : measurable_space α} {f : α → M} {μ : measure_theory.measure α} [has_measurable_add M] (hf : ae_measurable f μ) (c : M) :
ae_measurable (λ (x : α), c + f x) μ
@[measurability]
theorem measurable.add_const {M : Type u_1} {α : Type u_2} [measurable_space M] [has_add M] {m : measurable_space α} {f : α → M} [has_measurable_add M] (hf : measurable f) (c : M) :
measurable (λ (x : α), f x + c)
@[measurability]
theorem measurable.mul_const {M : Type u_1} {α : Type u_2} [measurable_space M] [has_mul M] {m : measurable_space α} {f : α → M} [has_measurable_mul M] (hf : measurable f) (c : M) :
measurable (λ (x : α), f x * c)
@[measurability]
theorem ae_measurable.mul_const {M : Type u_1} {α : Type u_2} [measurable_space M] [has_mul M] {m : measurable_space α} {f : α → M} {μ : measure_theory.measure α} [has_measurable_mul M] (hf : ae_measurable f μ) (c : M) :
ae_measurable (λ (x : α), f x * c) μ
@[measurability]
theorem ae_measurable.add_const {M : Type u_1} {α : Type u_2} [measurable_space M] [has_add M] {m : measurable_space α} {f : α → M} {μ : measure_theory.measure α} [has_measurable_add M] (hf : ae_measurable f μ) (c : M) :
ae_measurable (λ (x : α), f x + c) μ
@[measurability]
theorem measurable.add' {M : Type u_1} {α : Type u_2} [measurable_space M] [has_add M] {m : measurable_space α} {f g : α → M} [has_measurable_add₂ M] (hf : measurable f) (hg : measurable g) :
@[measurability]
theorem measurable.mul' {M : Type u_1} {α : Type u_2} [measurable_space M] [has_mul M] {m : measurable_space α} {f g : α → M} [has_measurable_mul₂ M] (hf : measurable f) (hg : measurable g) :
@[measurability]
theorem measurable.add {M : Type u_1} {α : Type u_2} [measurable_space M] [has_add M] {m : measurable_space α} {f g : α → M} [has_measurable_add₂ M] (hf : measurable f) (hg : measurable g) :
measurable (λ (a : α), f a + g a)
@[measurability]
theorem measurable.mul {M : Type u_1} {α : Type u_2} [measurable_space M] [has_mul M] {m : measurable_space α} {f g : α → M} [has_measurable_mul₂ 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} [measurable_space M] [has_mul M] {m : measurable_space α} {f g : α → M} {μ : measure_theory.measure α} [has_measurable_mul₂ M] (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (f * g) μ
@[measurability]
theorem ae_measurable.add' {M : Type u_1} {α : Type u_2} [measurable_space M] [has_add M] {m : measurable_space α} {f g : α → M} {μ : measure_theory.measure α} [has_measurable_add₂ M] (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (f + g) μ
@[measurability]
theorem ae_measurable.add {M : Type u_1} {α : Type u_2} [measurable_space M] [has_add M] {m : measurable_space α} {f g : α → M} {μ : measure_theory.measure α} [has_measurable_add₂ M] (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (a : α), f a + g a) μ
@[measurability]
theorem ae_measurable.mul {M : Type u_1} {α : Type u_2} [measurable_space M] [has_mul M] {m : measurable_space α} {f g : α → M} {μ : measure_theory.measure α} [has_measurable_mul₂ M] (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (a : α), f a * g a) μ
@[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} [div_inv_monoid G] [measurable_space G] [has_measurable_mul G] (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} [sub_neg_monoid G] [measurable_space G] [has_measurable_add G] (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) [measurable_space β] [measurable_space γ] [has_pow β γ] :
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]

monoid.has_pow is measurable.

Equations
@[measurability]
theorem measurable.pow {β : Type u_1} {γ : Type u_2} {α : Type u_3} [measurable_space β] [measurable_space γ] [has_pow β γ] [has_measurable_pow β γ] {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} [measurable_space β] [measurable_space γ] [has_pow β γ] [has_measurable_pow β γ] {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} {g : α → γ} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (x : α), f x ^ g x) μ
@[measurability]
theorem measurable.pow_const {β : Type u_1} {γ : Type u_2} {α : Type u_3} [measurable_space β] [measurable_space γ] [has_pow β γ] [has_measurable_pow β γ] {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} [measurable_space β] [measurable_space γ] [has_pow β γ] [has_measurable_pow β γ] {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} (hf : ae_measurable f μ) (c : γ) :
ae_measurable (λ (x : α), f x ^ c) μ
@[measurability]
theorem measurable.const_pow {β : Type u_1} {γ : Type u_2} {α : Type u_3} [measurable_space β] [measurable_space γ] [has_pow β γ] [has_measurable_pow β γ] {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} [measurable_space β] [measurable_space γ] [has_pow β γ] [has_measurable_pow β γ] {m : measurable_space α} {μ : measure_theory.measure α} {g : α → γ} (hg : ae_measurable g μ) (c : β) :
ae_measurable (λ (x : α), c ^ g x) μ
@[class]
structure has_measurable_sub (G : Type u_1) [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 of this typeclass
@[class]
structure has_measurable_sub₂ (G : Type u_1) [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 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 ((/) 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} [measurable_space G] [has_div G] {m : measurable_space α} {f : α → G} [has_measurable_div G] (hf : measurable f) (c : G) :
measurable (λ (x : α), c / f x)
@[measurability]
theorem measurable.const_sub {G : Type u_1} {α : Type u_2} [measurable_space G] [has_sub G] {m : measurable_space α} {f : α → G} [has_measurable_sub G] (hf : measurable f) (c : G) :
measurable (λ (x : α), c - f x)
@[measurability]
theorem ae_measurable.const_sub {G : Type u_1} {α : Type u_2} [measurable_space G] [has_sub G] {m : measurable_space α} {f : α → G} {μ : measure_theory.measure α} [has_measurable_sub G] (hf : ae_measurable f μ) (c : G) :
ae_measurable (λ (x : α), c - f x) μ
@[measurability]
theorem ae_measurable.const_div {G : Type u_1} {α : Type u_2} [measurable_space G] [has_div G] {m : measurable_space α} {f : α → G} {μ : measure_theory.measure α} [has_measurable_div G] (hf : ae_measurable f μ) (c : G) :
ae_measurable (λ (x : α), c / f x) μ
@[measurability]
theorem measurable.sub_const {G : Type u_1} {α : Type u_2} [measurable_space G] [has_sub G] {m : measurable_space α} {f : α → G} [has_measurable_sub G] (hf : measurable f) (c : G) :
measurable (λ (x : α), f x - c)
@[measurability]
theorem measurable.div_const {G : Type u_1} {α : Type u_2} [measurable_space G] [has_div G] {m : measurable_space α} {f : α → G} [has_measurable_div G] (hf : measurable f) (c : G) :
measurable (λ (x : α), f x / c)
@[measurability]
theorem ae_measurable.sub_const {G : Type u_1} {α : Type u_2} [measurable_space G] [has_sub G] {m : measurable_space α} {f : α → G} {μ : measure_theory.measure α} [has_measurable_sub G] (hf : ae_measurable f μ) (c : G) :
ae_measurable (λ (x : α), f x - c) μ
@[measurability]
theorem ae_measurable.div_const {G : Type u_1} {α : Type u_2} [measurable_space G] [has_div G] {m : measurable_space α} {f : α → G} {μ : measure_theory.measure α} [has_measurable_div G] (hf : ae_measurable f μ) (c : G) :
ae_measurable (λ (x : α), f x / c) μ
@[measurability]
theorem measurable.sub' {G : Type u_1} {α : Type u_2} [measurable_space G] [has_sub G] {m : measurable_space α} {f g : α → G} [has_measurable_sub₂ G] (hf : measurable f) (hg : measurable g) :
@[measurability]
theorem measurable.div' {G : Type u_1} {α : Type u_2} [measurable_space G] [has_div G] {m : measurable_space α} {f g : α → G} [has_measurable_div₂ G] (hf : measurable f) (hg : measurable g) :
@[measurability]
theorem measurable.div {G : Type u_1} {α : Type u_2} [measurable_space G] [has_div G] {m : measurable_space α} {f g : α → G} [has_measurable_div₂ G] (hf : measurable f) (hg : measurable g) :
measurable (λ (a : α), f a / g a)
@[measurability]
theorem measurable.sub {G : Type u_1} {α : Type u_2} [measurable_space G] [has_sub G] {m : measurable_space α} {f g : α → G} [has_measurable_sub₂ 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} [measurable_space G] [has_div G] {m : measurable_space α} {f g : α → G} {μ : measure_theory.measure α} [has_measurable_div₂ G] (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (f / g) μ
@[measurability]
theorem ae_measurable.sub' {G : Type u_1} {α : Type u_2} [measurable_space G] [has_sub G] {m : measurable_space α} {f g : α → G} {μ : measure_theory.measure α} [has_measurable_sub₂ G] (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (f - g) μ
@[measurability]
theorem ae_measurable.sub {G : Type u_1} {α : Type u_2} [measurable_space G] [has_sub G] {m : measurable_space α} {f g : α → G} {μ : measure_theory.measure α} [has_measurable_sub₂ G] (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (a : α), f a - g a) μ
@[measurability]
theorem ae_measurable.div {G : Type u_1} {α : Type u_2} [measurable_space G] [has_div G] {m : measurable_space α} {f g : α → G} {μ : measure_theory.measure α} [has_measurable_div₂ G] (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (a : α), f a / g a) μ
@[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} [measurable_space E] [add_group E] [measurable_singleton_class E] [has_measurable_sub₂ 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} [measurable_space E] [measurable_singleton_class E] [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 α} [measurable_space E] [add_group E] [measurable_singleton_class E] [has_measurable_sub₂ 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] [measurable_space G] :
Prop

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] [measurable_space G] :
Prop

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

Instances of this typeclass
@[measurability]
theorem measurable.inv {G : Type u_1} {α : Type u_2} [has_inv G] [measurable_space G] [has_measurable_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] [measurable_space G] [has_measurable_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] [measurable_space G] [has_measurable_neg G] {m : measurable_space α} {f : α → G} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :
ae_measurable (λ (x : α), -f x) μ
@[measurability]
theorem ae_measurable.inv {G : Type u_1} {α : Type u_2} [has_inv G] [measurable_space G] [has_measurable_inv G] {m : measurable_space α} {f : α → G} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :
ae_measurable (λ (x : α), (f x)⁻¹) μ
@[simp]
theorem measurable_inv_iff {α : Type u_2} {m : measurable_space α} {G : Type u_1} [group G] [measurable_space G] [has_measurable_inv G] {f : α → G} :
measurable (λ (x : α), (f x)⁻¹) measurable f
@[simp]
theorem measurable_neg_iff {α : Type u_2} {m : measurable_space α} {G : Type u_1} [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_2} {m : measurable_space α} {μ : measure_theory.measure α} {G : Type u_1} [group G] [measurable_space G] [has_measurable_inv G] {f : α → G} :
ae_measurable (λ (x : α), (f x)⁻¹) μ ae_measurable f μ
@[simp]
theorem ae_measurable_neg_iff {α : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {G : Type u_1} [add_group G] [measurable_space G] [has_measurable_neg G] {f : α → G} :
ae_measurable (λ (x : α), -f x) μ ae_measurable f μ
@[simp]
theorem measurable_inv_iff₀ {α : Type u_2} {m : measurable_space α} {G₀ : Type u_1} [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_2} {m : measurable_space α} {μ : measure_theory.measure α} {G₀ : Type u_1} [group_with_zero G₀] [measurable_space G₀] [has_measurable_inv G₀] {f : α → G₀} :
ae_measurable (λ (x : α), (f x)⁻¹) μ ae_measurable f μ
@[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.neg {G : Type u_1} [has_neg G] [measurable_space G] [has_measurable_neg G] {s : set G} (hs : measurable_set s) :
@[class]
structure has_measurable_vadd (M : Type u_1) (α : Type u_2) [has_vadd M α] [measurable_space M] [measurable_space α] :
Prop

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) [has_smul 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 of this typeclass
@[class]
structure has_measurable_vadd₂ (M : Type u_1) (α : Type u_2) [has_vadd M α] [measurable_space M] [measurable_space α] :
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) [has_smul 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 of this typeclass
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def submonoid.has_measurable_smul {M : Type u_1} {α : Type u_2} [measurable_space M] [measurable_space α] [monoid M] [mul_action M α] [has_measurable_smul M α] (s : submonoid M) :
@[protected, instance]
@[protected, instance]
def subgroup.has_measurable_smul {G : Type u_1} {α : Type u_2} [measurable_space G] [measurable_space α] [group G] [mul_action G α] [has_measurable_smul G α] (s : subgroup G) :
@[protected, instance]
@[measurability]
theorem measurable.smul {M : Type u_1} {β : Type u_2} {α : Type u_3} [measurable_space M] [measurable_space β] [has_smul M β] {m : measurable_space α} {f : α → M} {g : α → β} [has_measurable_smul₂ M β] (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} [measurable_space M] [measurable_space β] [has_vadd M β] {m : measurable_space α} {f : α → M} {g : α → β} [has_measurable_vadd₂ M β] (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} [measurable_space M] [measurable_space β] [has_vadd M β] {m : measurable_space α} {f : α → M} {g : α → β} [has_measurable_vadd₂ M β] {μ : measure_theory.measure α} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (x : α), f x +ᵥ g x) μ
@[measurability]
theorem ae_measurable.smul {M : Type u_1} {β : Type u_2} {α : Type u_3} [measurable_space M] [measurable_space β] [has_smul M β] {m : measurable_space α} {f : α → M} {g : α → β} [has_measurable_smul₂ M β] {μ : measure_theory.measure α} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (x : α), f x g x) μ
@[protected, instance]
@[protected, instance]
@[measurability]
theorem measurable.vadd_const {M : Type u_1} {β : Type u_2} {α : Type u_3} [measurable_space M] [measurable_space β] [has_vadd M β] {m : measurable_space α} {f : α → M} [has_measurable_vadd 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} [measurable_space M] [measurable_space β] [has_smul M β] {m : measurable_space α} {f : α → M} [has_measurable_smul 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} [measurable_space M] [measurable_space β] [has_vadd M β] {m : measurable_space α} {f : α → M} [has_measurable_vadd M β] {μ : measure_theory.measure α} (hf : ae_measurable f μ) (y : β) :
ae_measurable (λ (x : α), f x +ᵥ y) μ
@[measurability]
theorem ae_measurable.smul_const {M : Type u_1} {β : Type u_2} {α : Type u_3} [measurable_space M] [measurable_space β] [has_smul M β] {m : measurable_space α} {f : α → M} [has_measurable_smul M β] {μ : measure_theory.measure α} (hf : ae_measurable f μ) (y : β) :
ae_measurable (λ (x : α), f x y) μ
@[measurability]
theorem measurable.const_vadd' {M : Type u_1} {β : Type u_2} {α : Type u_3} [measurable_space M] [measurable_space β] [has_vadd M β] {m : measurable_space α} {g : α → β} [has_measurable_vadd M β] (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} [measurable_space M] [measurable_space β] [has_smul M β] {m : measurable_space α} {g : α → β} [has_measurable_smul M β] (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} [measurable_space M] [measurable_space β] [has_vadd M β] {m : measurable_space α} {g : α → β} [has_measurable_vadd M β] (hg : measurable g) (c : M) :
@[measurability]
theorem measurable.const_smul {M : Type u_1} {β : Type u_2} {α : Type u_3} [measurable_space M] [measurable_space β] [has_smul M β] {m : measurable_space α} {g : α → β} [has_measurable_smul M β] (hg : measurable g) (c : M) :
@[measurability]
theorem ae_measurable.const_smul' {M : Type u_1} {β : Type u_2} {α : Type u_3} [measurable_space M] [measurable_space β] [has_smul M β] {m : measurable_space α} {g : α → β} [has_measurable_smul M β] {μ : measure_theory.measure α} (hg : ae_measurable g μ) (c : M) :
ae_measurable (λ (x : α), c g x) μ
@[measurability]
theorem ae_measurable.const_vadd' {M : Type u_1} {β : Type u_2} {α : Type u_3} [measurable_space M] [measurable_space β] [has_vadd M β] {m : measurable_space α} {g : α → β} [has_measurable_vadd M β] {μ : measure_theory.measure α} (hg : ae_measurable g μ) (c : M) :
ae_measurable (λ (x : α), c +ᵥ g x) μ
@[measurability]
theorem ae_measurable.const_smul {M : Type u_1} {β : Type u_2} {α : Type u_3} [measurable_space M] [measurable_space β] [has_smul M β] {m : measurable_space α} {g : α → β} [has_measurable_smul M β] {μ : measure_theory.measure α} (hf : ae_measurable g μ) (c : M) :
@[measurability]
theorem ae_measurable.const_vadd {M : Type u_1} {β : Type u_2} {α : Type u_3} [measurable_space M] [measurable_space β] [has_vadd M β] {m : measurable_space α} {g : α → β} [has_measurable_vadd M β] {μ : measure_theory.measure α} (hf : ae_measurable g μ) (c : M) :
@[protected, instance]
def pi.has_measurable_smul {M : Type u_1} [measurable_space M] {ι : Type u_2} {α : ι → Type u_3} [Π (i : ι), has_smul M (α i)] [Π (i : ι), measurable_space (α i)] [∀ (i : ι), has_measurable_smul M (α i)] :
has_measurable_smul M (Π (i : ι), α i)
@[protected, instance]
def pi.has_measurable_vadd {M : Type u_1} [measurable_space M] {ι : Type u_2} {α : ι → Type u_3} [Π (i : ι), has_vadd M (α i)] [Π (i : ι), measurable_space (α i)] [∀ (i : ι), has_measurable_vadd M (α i)] :
has_measurable_vadd M (Π (i : ι), α i)
theorem measurable_const_vadd_iff {β : Type u_2} {α : Type u_3} [measurable_space β] [measurable_space α] {f : α → β} {G : Type u_4} [add_group G] [measurable_space G] [add_action G β] [has_measurable_vadd G β] (c : G) :
measurable (λ (x : α), c +ᵥ f x) measurable f
theorem measurable_const_smul_iff {β : Type u_2} {α : Type u_3} [measurable_space β] [measurable_space α] {f : α → β} {G : Type u_4} [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_vadd_iff {β : Type u_2} {α : Type u_3} [measurable_space β] [measurable_space α] {f : α → β} {μ : measure_theory.measure α} {G : Type u_4} [add_group G] [measurable_space G] [add_action G β] [has_measurable_vadd G β] (c : G) :
ae_measurable (λ (x : α), c +ᵥ f x) μ ae_measurable f μ
theorem ae_measurable_const_smul_iff {β : Type u_2} {α : Type u_3} [measurable_space β] [measurable_space α] {f : α → β} {μ : measure_theory.measure α} {G : Type u_4} [group G] [measurable_space G] [mul_action G β] [has_measurable_smul G β] (c : G) :
ae_measurable (λ (x : α), c f x) μ ae_measurable f μ
@[protected, instance]
Equations
@[protected, instance]
def units.has_measurable_smul {M : Type u_1} {β : Type u_2} [measurable_space M] [measurable_space β] [monoid M] [mul_action M β] [has_measurable_smul M β] :
@[protected, instance]
theorem is_unit.measurable_const_smul_iff {M : Type u_1} {β : Type u_2} {α : Type u_3} [measurable_space M] [measurable_space β] [monoid M] [mul_action M β] [has_measurable_smul M β] [measurable_space α] {f : α → β} {c : M} (hc : is_unit c) :
measurable (λ (x : α), c f x) measurable f
theorem is_add_unit.measurable_const_vadd_iff {M : Type u_1} {β : Type u_2} {α : Type u_3} [measurable_space M] [measurable_space β] [add_monoid M] [add_action M β] [has_measurable_vadd M β] [measurable_space α] {f : α → β} {c : M} (hc : is_add_unit c) :
measurable (λ (x : α), c +ᵥ f x) measurable f
theorem is_add_unit.ae_measurable_const_vadd_iff {M : Type u_1} {β : Type u_2} {α : Type u_3} [measurable_space M] [measurable_space β] [add_monoid M] [add_action M β] [has_measurable_vadd M β] [measurable_space α] {f : α → β} {μ : measure_theory.measure α} {c : M} (hc : is_add_unit c) :
ae_measurable (λ (x : α), c +ᵥ f x) μ ae_measurable f μ
theorem is_unit.ae_measurable_const_smul_iff {M : Type u_1} {β : Type u_2} {α : Type u_3} [measurable_space M] [measurable_space β] [monoid M] [mul_action M β] [has_measurable_smul M β] [measurable_space α] {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_2} {α : Type u_3} [measurable_space β] [measurable_space α] {f : α → β} {G₀ : Type u_5} [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_2} {α : Type u_3} [measurable_space β] [measurable_space α] {f : α → β} {μ : measure_theory.measure α} {G₀ : Type u_5} [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 μ

Opposite monoid #

@[protected, instance]

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

@[protected, instance]

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

Big operators: and #

@[measurability]
theorem list.measurable_prod' {M : Type u_1} {α : Type u_2} [monoid M] [measurable_space M] [has_measurable_mul₂ M] {m : measurable_space α} (l : list (α → M)) (hl : ∀ (f : α → M), f lmeasurable f) :
@[measurability]
theorem list.measurable_sum' {M : Type u_1} {α : Type u_2} [add_monoid M] [measurable_space M] [has_measurable_add₂ M] {m : measurable_space α} (l : list (α → M)) (hl : ∀ (f : α → M), f lmeasurable f) :
@[measurability]
theorem list.ae_measurable_prod' {M : Type u_1} {α : Type u_2} [monoid M] [measurable_space M] [has_measurable_mul₂ M] {m : measurable_space α} {μ : measure_theory.measure α} (l : list (α → M)) (hl : ∀ (f : α → M), f lae_measurable f μ) :
@[measurability]
theorem list.ae_measurable_sum' {M : Type u_1} {α : Type u_2} [add_monoid M] [measurable_space M] [has_measurable_add₂ M] {m : measurable_space α} {μ : measure_theory.measure α} (l : list (α → M)) (hl : ∀ (f : α → M), f lae_measurable f μ) :
@[measurability]
theorem list.measurable_prod {M : Type u_1} {α : Type u_2} [monoid M] [measurable_space M] [has_measurable_mul₂ M] {m : measurable_space α} (l : list (α → M)) (hl : ∀ (f : α → M), f lmeasurable f) :
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] [measurable_space M] [has_measurable_add₂ M] {m : measurable_space α} (l : list (α → M)) (hl : ∀ (f : α → M), f lmeasurable f) :
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] [measurable_space M] [has_measurable_mul₂ M] {m : measurable_space α} {μ : measure_theory.measure α} (l : list (α → M)) (hl : ∀ (f : α → M), f lae_measurable f μ) :
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] [measurable_space M] [has_measurable_add₂ M] {m : measurable_space α} {μ : measure_theory.measure α} (l : list (α → M)) (hl : ∀ (f : α → M), f lae_measurable f μ) :
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] [measurable_space M] [has_measurable_mul₂ M] {m : measurable_space α} (l : multiset (α → M)) (hl : ∀ (f : α → M), f lmeasurable f) :
@[measurability]
theorem multiset.measurable_sum' {M : Type u_1} {α : Type u_3} [add_comm_monoid M] [measurable_space M] [has_measurable_add₂ M] {m : measurable_space α} (l : multiset (α → M)) (hl : ∀ (f : α → M), f lmeasurable f) :
@[measurability]
theorem multiset.ae_measurable_prod' {M : Type u_1} {α : Type u_3} [comm_monoid M] [measurable_space M] [has_measurable_mul₂ M] {m : measurable_space α} {μ : measure_theory.measure α} (l : multiset (α → M)) (hl : ∀ (f : α → M), f lae_measurable f μ) :
@[measurability]
theorem multiset.ae_measurable_sum' {M : Type u_1} {α : Type u_3} [add_comm_monoid M] [measurable_space M] [has_measurable_add₂ M] {m : measurable_space α} {μ : measure_theory.measure α} (l : multiset (α → M)) (hl : ∀ (f : α → M), f lae_measurable f μ) :
@[measurability]
theorem multiset.measurable_prod {M : Type u_1} {α : Type u_3} [comm_monoid M] [measurable_space M] [has_measurable_mul₂ M] {m : measurable_space α} (s : multiset (α → M)) (hs : ∀ (f : α → M), f smeasurable f) :
measurable (λ (x : α), (multiset.map (λ (f : α → M), f x) s).prod)
@[measurability]
theorem multiset.measurable_sum {M : Type u_1} {α : Type u_3} [add_comm_monoid M] [measurable_space M] [has_measurable_add₂ M] {m : measurable_space α} (s : multiset (α → M)) (hs : ∀ (f : α → M), f smeasurable f) :
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] [measurable_space M] [has_measurable_mul₂ M] {m : measurable_space α} {μ : measure_theory.measure α} (s : multiset (α → M)) (hs : ∀ (f : α → M), f sae_measurable f μ) :
ae_measurable (λ (x : α), (multiset.map (λ (f : α → M), f x) s).prod) μ
@[measurability]
theorem multiset.ae_measurable_sum {M : Type u_1} {α : Type u_3} [add_comm_monoid M] [measurable_space M] [has_measurable_add₂ M] {m : measurable_space α} {μ : measure_theory.measure α} (s : multiset (α → M)) (hs : ∀ (f : α → M), f sae_measurable f μ) :
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} [add_comm_monoid M] [measurable_space M] [has_measurable_add₂ M] {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] [measurable_space M] [has_measurable_mul₂ 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} [add_comm_monoid M] [measurable_space M] [has_measurable_add₂ M] {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] [measurable_space M] [has_measurable_mul₂ 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} [add_comm_monoid M] [measurable_space M] [has_measurable_add₂ M] {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] [measurable_space M] [has_measurable_mul₂ 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] [measurable_space M] [has_measurable_mul₂ 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} [add_comm_monoid M] [measurable_space M] [has_measurable_add₂ M] {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)) μ