Typeclasses for measurability of operations #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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_mulsays that both left and right multiplication are measurable;has_measurable_mul₂says thatλ p : α × α, p.1 * p.2is 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
powandsmul. - Use
@[to_additive]to sendhas_measurable_powtohas_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]
- measurable_const_add : ∀ (c : M), measurable (has_add.add c)
- 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₂.
@[class]
- measurable_add : measurable (λ (p : M × M), p.fst + p.snd)
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.
@[class]
- measurable_const_mul : ∀ (c : M), measurable (has_mul.mul c)
- 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₂.
@[class]
- measurable_mul : measurable (λ (p : M × M), p.fst * p.snd)
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) :
measurable (f + 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) :
measurable (f * 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
has_measurable_mul₂.to_has_measurable_mul
{M : Type u_1}
[measurable_space M]
[has_mul M]
[has_measurable_mul₂ M] :
@[protected, instance]
def
has_measurable_add₂.to_has_measurable_add
{M : Type u_1}
[measurable_space M]
[has_add M]
[has_measurable_add₂ M] :
@[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 β γ] :
- measurable_pow : measurable (λ (p : β × γ), p.fst ^ p.snd)
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]
[measurable_space M]
[has_measurable_mul₂ M] :
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]
- 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₂.
@[class]
- measurable_sub : measurable (λ (p : G × G), p.fst - p.snd)
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]
- measurable_const_div : ∀ (c : G₀), measurable (has_div.div c)
- 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]
- measurable_div : measurable (λ (p : G₀ × G₀), p.fst / p.snd)
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) :
measurable (f - 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 (f / 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
has_measurable_div₂.to_has_measurable_div
{G : Type u_1}
[measurable_space G]
[has_div G]
[has_measurable_div₂ G] :
@[protected, instance]
def
has_measurable_sub₂.to_has_measurable_sub
{G : Type u_1}
[measurable_space G]
[has_sub G]
[has_measurable_sub₂ G] :
@[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
null_measurable_set_eq_fun
{α : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_1}
[measurable_space E]
[add_group E]
[measurable_singleton_class E]
[has_measurable_sub₂ E]
{f g : α → E}
(hf : ae_measurable f μ)
(hg : ae_measurable g μ) :
measure_theory.null_measurable_set {x : α | f x = g x} μ
theorem
measurable_set_eq_fun_of_countable
{α : Type u_2}
{m : measurable_space α}
{E : Type u_1}
[measurable_space E]
[measurable_singleton_class E]
[countable 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) :
@[class]
- measurable_neg : measurable has_neg.neg
We say that a type has_measurable_neg if x ↦ -x is a measurable function.
Instances of this typeclass
@[class]
- measurable_inv : measurable has_inv.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)
[measurable_space G]
[div_inv_monoid G]
[has_measurable_mul G]
[has_measurable_inv G] :
@[protected, instance]
def
has_measurable_sub_of_add_neg
(G : Type u_1)
[measurable_space G]
[sub_neg_monoid G]
[has_measurable_add G]
[has_measurable_neg G] :
@[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.inv
{G : Type u_1}
[has_inv G]
[measurable_space G]
[has_measurable_inv G]
{s : set G}
(hs : measurable_set s) :
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) :
measurable_set (-s)
@[protected, instance]
def
div_inv_monoid.has_measurable_zpow
(G : Type u)
[div_inv_monoid G]
[measurable_space G]
[has_measurable_mul₂ G]
[has_measurable_inv G] :
div_inv_monoid.has_pow is measurable.
Equations
@[protected, instance]
def
has_measurable_div₂_of_mul_inv
(G : Type u_1)
[measurable_space G]
[div_inv_monoid G]
[has_measurable_mul₂ G]
[has_measurable_inv G] :
@[protected, instance]
def
has_measurable_div₂_of_add_neg
(G : Type u_1)
[measurable_space G]
[sub_neg_monoid G]
[has_measurable_add₂ G]
[has_measurable_neg G] :
@[class]
structure
has_measurable_vadd
(M : Type u_1)
(α : Type u_2)
[has_vadd M α]
[measurable_space M]
[measurable_space α] :
Prop
- measurable_const_vadd : ∀ (c : M), measurable (has_vadd.vadd c)
- 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.
@[class]
structure
has_measurable_smul
(M : Type u_1)
(α : Type u_2)
[has_smul M α]
[measurable_space M]
[measurable_space α] :
Prop
- measurable_const_smul : ∀ (c : M), measurable (has_smul.smul c)
- 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
- has_measurable_smul₂.to_has_measurable_smul
- has_continuous_smul.has_measurable_smul
- has_measurable_smul_of_mul
- submonoid.has_measurable_smul
- subgroup.has_measurable_smul
- pi.has_measurable_smul
- units.has_measurable_smul
- has_measurable_smul.op
- has_measurable_smul_opposite_of_mul
- quotient_group.has_measurable_smul
@[class]
structure
has_measurable_vadd₂
(M : Type u_1)
(α : Type u_2)
[has_vadd M α]
[measurable_space M]
[measurable_space α] :
Prop
- measurable_vadd : measurable (function.uncurry has_vadd.vadd)
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
- measurable_smul : measurable (function.uncurry has_smul.smul)
We say that the action of M on α has_measurable_smul₂ if the map
(c, x) ↦ c • x is a measurable function.
@[protected, instance]
def
has_measurable_vadd_of_add
(M : Type u_1)
[has_add M]
[measurable_space M]
[has_measurable_add M] :
@[protected, instance]
def
has_measurable_smul_of_mul
(M : Type u_1)
[has_mul M]
[measurable_space M]
[has_measurable_mul M] :
@[protected, instance]
def
has_measurable_smul₂_of_mul
(M : Type u_1)
[has_mul M]
[measurable_space M]
[has_measurable_mul₂ M] :
@[protected, instance]
def
has_measurable_smul₂_of_add
(M : Type u_1)
[has_add M]
[measurable_space M]
[has_measurable_add₂ M] :
@[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]
def
add_submonoid.has_measurable_vadd
{M : Type u_1}
{α : Type u_2}
[measurable_space M]
[measurable_space α]
[add_monoid M]
[add_action M α]
[has_measurable_vadd M α]
(s : add_submonoid M) :
@[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]
def
add_subgroup.has_measurable_vadd
{G : Type u_1}
{α : Type u_2}
[measurable_space G]
[measurable_space α]
[add_group G]
[add_action G α]
[has_measurable_vadd G α]
(s : add_subgroup G) :
@[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]
def
has_measurable_smul₂.to_has_measurable_smul
{M : Type u_1}
{β : Type u_2}
[measurable_space M]
[measurable_space β]
[has_smul M β]
[has_measurable_smul₂ M β] :
@[protected, instance]
def
has_measurable_vadd₂.to_has_measurable_vadd
{M : Type u_1}
{β : Type u_2}
[measurable_space M]
[measurable_space β]
[has_vadd M β]
[has_measurable_vadd₂ M β] :
@[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) :
measurable (c +ᵥ g)
@[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 (c • g)
@[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) :
ae_measurable (c • g) μ
@[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) :
ae_measurable (c +ᵥ g) μ
@[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)
@[protected, instance]
def
add_monoid.has_measurable_smul_nat₂
(M : Type u_1)
[add_monoid M]
[measurable_space M]
[has_measurable_add₂ M] :
add_monoid.has_smul_nat is measurable.
@[protected, instance]
def
sub_neg_monoid.has_measurable_smul_int₂
(M : Type u_1)
[sub_neg_monoid M]
[measurable_space M]
[has_measurable_add₂ M]
[has_measurable_neg M] :
sub_neg_monoid.has_smul_int is measurable.
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]
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]
def
add_units.has_measurable_vadd
{M : Type u_1}
{β : Type u_2}
[measurable_space M]
[measurable_space β]
[add_monoid M]
[add_action M β]
[has_measurable_vadd M β] :
has_measurable_vadd (add_units M) β
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]
@[protected, instance]
@[protected, instance]
def
mul_opposite.has_measurable_mul
{M : Type u_1}
[has_mul M]
[measurable_space M]
[has_measurable_mul M] :
@[protected, instance]
def
add_opposite.has_measurable_add
{M : Type u_1}
[has_add M]
[measurable_space M]
[has_measurable_add M] :
@[protected, instance]
def
add_opposite.has_measurable_mul₂
{M : Type u_1}
[has_add M]
[measurable_space M]
[has_measurable_add₂ M] :
@[protected, instance]
def
mul_opposite.has_measurable_mul₂
{M : Type u_1}
[has_mul M]
[measurable_space M]
[has_measurable_mul₂ M] :
@[protected, instance]
def
has_measurable_smul.op
{M : Type u_1}
{α : Type u_2}
[measurable_space M]
[measurable_space α]
[has_smul M α]
[has_smul Mᵐᵒᵖ α]
[is_central_scalar M α]
[has_measurable_smul M α] :
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}
[measurable_space M]
[measurable_space α]
[has_smul M α]
[has_smul Mᵐᵒᵖ α]
[is_central_scalar M α]
[has_measurable_smul₂ M α] :
If a scalar is central, then its right action is measurable when its left action is.
@[protected, instance]
def
has_measurable_vadd_opposite_of_add
{M : Type u_1}
[has_add M]
[measurable_space M]
[has_measurable_add M] :
@[protected, instance]
def
has_measurable_smul_opposite_of_mul
{M : Type u_1}
[has_mul M]
[measurable_space M]
[has_measurable_mul M] :
@[protected, instance]
def
has_measurable_smul₂_opposite_of_add
{M : Type u_1}
[has_add M]
[measurable_space M]
[has_measurable_add₂ M] :
@[protected, instance]
def
has_measurable_smul₂_opposite_of_mul
{M : Type u_1}
[has_mul M]
[measurable_space M]
[has_measurable_mul₂ M] :
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 ∈ l → measurable 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 ∈ l → measurable 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 ∈ l → ae_measurable f μ) :
ae_measurable 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 ∈ l → ae_measurable f μ) :
ae_measurable l.sum μ
@[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 ∈ l → measurable 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 ∈ l → measurable 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 ∈ l → ae_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 ∈ l → ae_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 ∈ l → measurable 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 ∈ l → measurable 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 ∈ l → ae_measurable f μ) :
ae_measurable l.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 α}
(l : multiset (α → M))
(hl : ∀ (f : α → M), f ∈ l → ae_measurable f μ) :
ae_measurable 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 α}
(s : multiset (α → M))
(hs : ∀ (f : α → M), f ∈ s → measurable 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 ∈ s → measurable 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 ∈ s → ae_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 ∈ s → ae_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 ∈ s → measurable (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 ∈ s → measurable (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 ∈ s → measurable (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 ∈ s → measurable (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 ∈ s → ae_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 ∈ s → ae_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 ∈ s → ae_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 ∈ s → ae_measurable (f i) μ) :
ae_measurable (λ (a : α), s.sum (λ (i : ι), f i a)) μ