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_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.
Tags #
measurable function, arithmetic operator
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.
Instances
@[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.
theorem
measurable.add
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[measurable_space M]
[has_add M]
[has_measurable_add₂ M]
{f g : α → M}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (a : α), f a + g a)
theorem
measurable.mul
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[measurable_space M]
[has_mul M]
[has_measurable_mul₂ M]
{f g : α → M}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (a : α), (f a) * g a)
theorem
ae_measurable.add
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[measurable_space M]
[has_add M]
[has_measurable_add₂ M]
{μ : measure_theory.measure α}
{f g : α → M}
(hf : ae_measurable f μ)
(hg : ae_measurable g μ) :
ae_measurable (λ (a : α), f a + g a) μ
theorem
ae_measurable.mul
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[measurable_space M]
[has_mul M]
[has_measurable_mul₂ M]
{μ : measure_theory.measure α}
{f g : α → M}
(hf : ae_measurable f μ)
(hg : ae_measurable g μ) :
ae_measurable (λ (a : α), (f a) * g a) μ
@[protected, instance]
def
has_measurable_mul₂.to_has_measurable_mul
{M : Type u_2}
[measurable_space M]
[has_mul M]
[has_measurable_mul₂ M] :
@[protected, instance]
def
has_measurable_add₂.to_has_measurable_add
{M : Type u_2}
[measurable_space M]
[has_add M]
[has_measurable_add₂ M] :
theorem
measurable.const_add
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[measurable_space M]
[has_add M]
[has_measurable_add M]
{f : α → M}
(hf : measurable f)
(c : M) :
measurable (λ (x : α), c + f x)
theorem
measurable.const_mul
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[measurable_space M]
[has_mul M]
[has_measurable_mul M]
{f : α → M}
(hf : measurable f)
(c : M) :
measurable (λ (x : α), c * f x)
theorem
ae_measurable.const_mul
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[measurable_space M]
[has_mul M]
[has_measurable_mul M]
{f : α → M}
{μ : measure_theory.measure α}
(hf : ae_measurable f μ)
(c : M) :
ae_measurable (λ (x : α), c * f x) μ
theorem
ae_measurable.const_add
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[measurable_space M]
[has_add M]
[has_measurable_add M]
{f : α → M}
{μ : measure_theory.measure α}
(hf : ae_measurable f μ)
(c : M) :
ae_measurable (λ (x : α), c + f x) μ
theorem
measurable.add_const
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[measurable_space M]
[has_add M]
[has_measurable_add M]
{f : α → M}
(hf : measurable f)
(c : M) :
measurable (λ (x : α), f x + c)
theorem
measurable.mul_const
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[measurable_space M]
[has_mul M]
[has_measurable_mul M]
{f : α → M}
(hf : measurable f)
(c : M) :
measurable (λ (x : α), (f x) * c)
theorem
ae_measurable.mul_const
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[measurable_space M]
[has_mul M]
[has_measurable_mul M]
{f : α → M}
{μ : measure_theory.measure α}
(hf : ae_measurable f μ)
(c : M) :
ae_measurable (λ (x : α), (f x) * c) μ
theorem
ae_measurable.add_const
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[measurable_space M]
[has_add M]
[has_measurable_add M]
{f : α → M}
{μ : measure_theory.measure α}
(hf : ae_measurable f μ)
(c : M) :
ae_measurable (λ (x : α), f x + c) μ
@[class]
structure
has_measurable_pow
(β : Type u_2)
(γ : Type u_3)
[measurable_space β]
[measurable_space γ]
[has_pow β γ] :
Type
- measurable_pow : measurable (λ (p : β × γ), p.fst ^ p.snd)
This class assumes that the map β × γ → β given by (x, y) ↦ x ^ y is measurable.
@[protected, instance]
def
has_measurable_mul.has_measurable_pow
(M : Type u_1)
[monoid M]
[measurable_space M]
[has_measurable_mul₂ M] :
Equations
theorem
measurable.pow
{α : Type u_1}
[measurable_space α]
{β : Type u_2}
{γ : Type u_3}
[measurable_space β]
[measurable_space γ]
[has_pow β γ]
[has_measurable_pow β γ]
{f : α → β}
{g : α → γ}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (x : α), f x ^ g x)
theorem
ae_measurable.pow
{α : Type u_1}
[measurable_space α]
{β : Type u_2}
{γ : Type u_3}
[measurable_space β]
[measurable_space γ]
[has_pow β γ]
[has_measurable_pow β γ]
{μ : measure_theory.measure α}
{f : α → β}
{g : α → γ}
(hf : ae_measurable f μ)
(hg : ae_measurable g μ) :
ae_measurable (λ (x : α), f x ^ g x) μ
theorem
measurable.pow_const
{α : Type u_1}
[measurable_space α]
{β : Type u_2}
{γ : Type u_3}
[measurable_space β]
[measurable_space γ]
[has_pow β γ]
[has_measurable_pow β γ]
{f : α → β}
(hf : measurable f)
(c : γ) :
measurable (λ (x : α), f x ^ c)
theorem
ae_measurable.pow_const
{α : Type u_1}
[measurable_space α]
{β : Type u_2}
{γ : Type u_3}
[measurable_space β]
[measurable_space γ]
[has_pow β γ]
[has_measurable_pow β γ]
{μ : measure_theory.measure α}
{f : α → β}
(hf : ae_measurable f μ)
(c : γ) :
ae_measurable (λ (x : α), f x ^ c) μ
theorem
measurable.const_pow
{α : Type u_1}
[measurable_space α]
{β : Type u_2}
{γ : Type u_3}
[measurable_space β]
[measurable_space γ]
[has_pow β γ]
[has_measurable_pow β γ]
{f : α → γ}
(hf : measurable f)
(c : β) :
measurable (λ (x : α), c ^ f x)
theorem
ae_measurable.const_pow
{α : Type u_1}
[measurable_space α]
{β : Type u_2}
{γ : Type u_3}
[measurable_space β]
[measurable_space γ]
[has_pow β γ]
[has_measurable_pow β γ]
{μ : measure_theory.measure α}
{f : α → γ}
(hf : ae_measurable f μ)
(c : β) :
ae_measurable (λ (x : α), c ^ f x) μ
@[class]
- 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.
@[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₂.
@[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
theorem
measurable.div
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[measurable_space G]
[has_div G]
[has_measurable_div₂ G]
{f g : α → G}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (a : α), f a / g a)
theorem
measurable.sub
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[measurable_space G]
[has_sub G]
[has_measurable_sub₂ G]
{f g : α → G}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (a : α), f a - g a)
theorem
ae_measurable.sub
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[measurable_space G]
[has_sub G]
[has_measurable_sub₂ G]
{f g : α → G}
{μ : measure_theory.measure α}
(hf : ae_measurable f μ)
(hg : ae_measurable g μ) :
ae_measurable (λ (a : α), f a - g a) μ
theorem
ae_measurable.div
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[measurable_space G]
[has_div G]
[has_measurable_div₂ G]
{f g : α → G}
{μ : measure_theory.measure α}
(hf : ae_measurable f μ)
(hg : ae_measurable g μ) :
ae_measurable (λ (a : α), f a / g a) μ
@[protected, instance]
def
has_measurable_div₂.to_has_measurable_div
{G : Type u_2}
[measurable_space G]
[has_div G]
[has_measurable_div₂ G] :
@[protected, instance]
def
has_measurable_sub₂.to_has_measurable_sub
{G : Type u_2}
[measurable_space G]
[has_sub G]
[has_measurable_sub₂ G] :
theorem
measurable.const_div
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[measurable_space G]
[has_div G]
[has_measurable_div G]
{f : α → G}
(hf : measurable f)
(c : G) :
measurable (λ (x : α), c / f x)
theorem
measurable.const_sub
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[measurable_space G]
[has_sub G]
[has_measurable_sub G]
{f : α → G}
(hf : measurable f)
(c : G) :
measurable (λ (x : α), c - f x)
theorem
ae_measurable.const_sub
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[measurable_space G]
[has_sub G]
[has_measurable_sub G]
{f : α → G}
{μ : measure_theory.measure α}
(hf : ae_measurable f μ)
(c : G) :
ae_measurable (λ (x : α), c - f x) μ
theorem
ae_measurable.const_div
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[measurable_space G]
[has_div G]
[has_measurable_div G]
{f : α → G}
{μ : measure_theory.measure α}
(hf : ae_measurable f μ)
(c : G) :
ae_measurable (λ (x : α), c / f x) μ
theorem
measurable.sub_const
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[measurable_space G]
[has_sub G]
[has_measurable_sub G]
{f : α → G}
(hf : measurable f)
(c : G) :
measurable (λ (x : α), f x - c)
theorem
measurable.div_const
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[measurable_space G]
[has_div G]
[has_measurable_div G]
{f : α → G}
(hf : measurable f)
(c : G) :
measurable (λ (x : α), f x / c)
theorem
ae_measurable.sub_const
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[measurable_space G]
[has_sub G]
[has_measurable_sub G]
{f : α → G}
{μ : measure_theory.measure α}
(hf : ae_measurable f μ)
(c : G) :
ae_measurable (λ (x : α), f x - c) μ
theorem
ae_measurable.div_const
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[measurable_space G]
[has_div G]
[has_measurable_div G]
{f : α → G}
{μ : measure_theory.measure α}
(hf : ae_measurable f μ)
(c : G) :
ae_measurable (λ (x : α), f x / c) μ
@[class]
- measurable_neg : measurable has_neg.neg
We say that a type has_measurable_neg if x ↦ -x is a measurable function.
Instances
@[class]
- measurable_inv : measurable has_inv.inv
We say that a type has_measurable_inv if x ↦ x⁻¹ is a measurable function.
@[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] :
theorem
measurable.inv
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[has_inv G]
[measurable_space G]
[has_measurable_inv G]
{f : α → G}
(hf : measurable f) :
measurable (λ (x : α), (f x)⁻¹)
theorem
measurable.neg
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[has_neg G]
[measurable_space G]
[has_measurable_neg G]
{f : α → G}
(hf : measurable f) :
measurable (λ (x : α), -f x)
theorem
ae_measurable.neg
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[has_neg G]
[measurable_space G]
[has_measurable_neg G]
{f : α → G}
{μ : measure_theory.measure α}
(hf : ae_measurable f μ) :
ae_measurable (λ (x : α), -f x) μ
theorem
ae_measurable.inv
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[has_inv G]
[measurable_space G]
[has_measurable_inv G]
{f : α → G}
{μ : measure_theory.measure α}
(hf : ae_measurable f μ) :
ae_measurable (λ (x : α), (f x)⁻¹) μ
@[simp]
theorem
measurable_inv_iff
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[group G]
[measurable_space G]
[has_measurable_inv G]
{f : α → G} :
measurable (λ (x : α), (f x)⁻¹) ↔ measurable f
@[simp]
theorem
measurable_neg_iff
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[add_group G]
[measurable_space G]
[has_measurable_neg G]
{f : α → G} :
measurable (λ (x : α), -f x) ↔ measurable f
@[simp]
theorem
ae_measurable_inv_iff
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[group G]
[measurable_space G]
[has_measurable_inv G]
{f : α → G}
{μ : measure_theory.measure α} :
ae_measurable (λ (x : α), (f x)⁻¹) μ ↔ ae_measurable f μ
@[simp]
theorem
ae_measurable_neg_iff
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[add_group G]
[measurable_space G]
[has_measurable_neg G]
{f : α → G}
{μ : measure_theory.measure α} :
ae_measurable (λ (x : α), -f x) μ ↔ ae_measurable f μ
@[simp]
theorem
measurable_inv_iff'
{α : Type u_1}
[measurable_space α]
{G₀ : Type u_2}
[group_with_zero G₀]
[measurable_space G₀]
[has_measurable_inv G₀]
{f : α → G₀} :
measurable (λ (x : α), (f x)⁻¹) ↔ measurable f
@[simp]
theorem
ae_measurable_inv_iff'
{α : Type u_1}
[measurable_space α]
{G₀ : Type u_2}
[group_with_zero G₀]
[measurable_space G₀]
[has_measurable_inv G₀]
{f : α → G₀}
{μ : measure_theory.measure α} :
ae_measurable (λ (x : α), (f x)⁻¹) μ ↔ ae_measurable f μ
@[protected, instance]
def
has_measurable_gpow
(G : Type u)
[div_inv_monoid G]
[measurable_space G]
[has_measurable_mul₂ G]
[has_measurable_inv G] :
Equations
- has_measurable_gpow G = let _inst : measurable_singleton_class ℤ := has_measurable_gpow._proof_1 in {measurable_pow := _}
@[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_smul
(M : Type u_2)
(α : Type u_3)
[has_scalar M α]
[measurable_space M]
[measurable_space α] :
Prop
- measurable_const_smul : ∀ (c : M), measurable (has_scalar.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.
@[class]
structure
has_measurable_smul₂
(M : Type u_2)
(α : Type u_3)
[has_scalar M α]
[measurable_space M]
[measurable_space α] :
Prop
- measurable_smul : measurable (function.uncurry has_scalar.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_smul_of_mul
(M : Type u_1)
[monoid M]
[measurable_space M]
[has_measurable_mul M] :
@[protected, instance]
def
has_measurable_smul₂_of_mul
(M : Type u_1)
[monoid M]
[measurable_space M]
[has_measurable_mul₂ M] :
theorem
measurable.smul
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
{β : Type u_3}
[measurable_space M]
[measurable_space β]
[has_scalar M β]
[has_measurable_smul₂ M β]
{f : α → M}
{g : α → β}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (x : α), f x • g x)
theorem
ae_measurable.smul
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
{β : Type u_3}
[measurable_space M]
[measurable_space β]
[has_scalar M β]
[has_measurable_smul₂ M β]
{f : α → M}
{g : α → β}
{μ : measure_theory.measure α}
(hf : ae_measurable f μ)
(hg : ae_measurable g μ) :
ae_measurable (λ (x : α), f x • g x) μ
@[protected, instance]
def
has_measurable_smul₂.to_has_measurable_smul
{M : Type u_2}
{β : Type u_3}
[measurable_space M]
[measurable_space β]
[has_scalar M β]
[has_measurable_smul₂ M β] :
theorem
measurable.smul_const
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
{β : Type u_3}
[measurable_space M]
[measurable_space β]
[has_scalar M β]
[has_measurable_smul M β]
{f : α → M}
(hf : measurable f)
(y : β) :
measurable (λ (x : α), f x • y)
theorem
ae_measurable.smul_const
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
{β : Type u_3}
[measurable_space M]
[measurable_space β]
[has_scalar M β]
[has_measurable_smul M β]
{μ : measure_theory.measure α}
{f : α → M}
(hf : ae_measurable f μ)
(y : β) :
ae_measurable (λ (x : α), f x • y) μ
theorem
measurable.const_smul'
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
{β : Type u_3}
[measurable_space M]
[measurable_space β]
[has_scalar M β]
[has_measurable_smul M β]
{f : α → β}
(hf : measurable f)
(c : M) :
measurable (λ (x : α), c • f x)
theorem
measurable.const_smul
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
{β : Type u_3}
[measurable_space M]
[measurable_space β]
[has_scalar M β]
[has_measurable_smul M β]
{f : α → β}
(hf : measurable f)
(c : M) :
measurable (c • f)
theorem
ae_measurable.const_smul'
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
{β : Type u_3}
[measurable_space M]
[measurable_space β]
[has_scalar M β]
[has_measurable_smul M β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : ae_measurable f μ)
(c : M) :
ae_measurable (λ (x : α), c • f x) μ
theorem
ae_measurable.const_smul
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
{β : Type u_3}
[measurable_space M]
[measurable_space β]
[has_scalar M β]
[has_measurable_smul M β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : ae_measurable f μ)
(c : M) :
ae_measurable (c • f) μ
@[simp]
theorem
units.measurable_const_smul_iff
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
{β : Type u_3}
[measurable_space M]
[measurable_space β]
[monoid M]
[mul_action M β]
[has_measurable_smul M β]
{f : α → β}
(u : units M) :
measurable (λ (x : α), ↑u • f x) ↔ measurable f
@[simp]
theorem
units.ae_measurable_const_smul_iff
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
{β : Type u_3}
[measurable_space M]
[measurable_space β]
[monoid M]
[mul_action M β]
[has_measurable_smul M β]
{f : α → β}
{μ : measure_theory.measure α}
(u : units M) :
ae_measurable (λ (x : α), ↑u • f x) μ ↔ ae_measurable f μ
theorem
is_unit.measurable_const_smul_iff
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
{β : Type u_3}
[measurable_space M]
[measurable_space β]
[monoid M]
[mul_action M β]
[has_measurable_smul M β]
{f : α → β}
{c : M}
(hc : is_unit c) :
measurable (λ (x : α), c • f x) ↔ measurable f
theorem
is_unit.ae_measurable_const_smul_iff
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
{β : Type u_3}
[measurable_space M]
[measurable_space β]
[monoid M]
[mul_action M β]
[has_measurable_smul M β]
{f : α → β}
{μ : measure_theory.measure α}
{c : M}
(hc : is_unit c) :
ae_measurable (λ (x : α), c • f x) μ ↔ ae_measurable f μ
theorem
measurable_const_smul_iff'
{α : Type u_1}
[measurable_space α]
{β : Type u_3}
[measurable_space β]
{f : α → β}
{G₀ : Type u_4}
[group_with_zero G₀]
[measurable_space G₀]
[mul_action G₀ β]
[has_measurable_smul G₀ β]
{c : G₀}
(hc : c ≠ 0) :
measurable (λ (x : α), c • f x) ↔ measurable f
theorem
ae_measurable_const_smul_iff'
{α : Type u_1}
[measurable_space α]
{β : Type u_3}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
{G₀ : Type u_4}
[group_with_zero G₀]
[measurable_space G₀]
[mul_action G₀ β]
[has_measurable_smul G₀ β]
{c : G₀}
(hc : c ≠ 0) :
ae_measurable (λ (x : α), c • f x) μ ↔ ae_measurable f μ
theorem
measurable_const_smul_iff
{α : Type u_1}
[measurable_space α]
{β : Type u_3}
[measurable_space β]
{f : α → β}
{G : Type u_5}
[group G]
[measurable_space G]
[mul_action G β]
[has_measurable_smul G β]
(c : G) :
measurable (λ (x : α), c • f x) ↔ measurable f
theorem
ae_measurable_const_smul_iff
{α : Type u_1}
[measurable_space α]
{β : Type u_3}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
{G : Type u_5}
[group G]
[measurable_space G]
[mul_action G β]
[has_measurable_smul G β]
(c : G) :
ae_measurable (λ (x : α), c • f x) μ ↔ ae_measurable f μ
Big operators: ∏ and ∑ #
theorem
list.measurable_prod'
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[monoid M]
[measurable_space M]
[has_measurable_mul₂ M]
(l : list (α → M))
(hl : ∀ (f : α → M), f ∈ l → measurable f) :
theorem
list.measurable_sum'
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[add_monoid M]
[measurable_space M]
[has_measurable_add₂ M]
(l : list (α → M))
(hl : ∀ (f : α → M), f ∈ l → measurable f) :
theorem
list.ae_measurable_prod'
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[monoid M]
[measurable_space M]
[has_measurable_mul₂ M]
{μ : measure_theory.measure α}
(l : list (α → M))
(hl : ∀ (f : α → M), f ∈ l → ae_measurable f μ) :
ae_measurable l.prod μ
theorem
list.ae_measurable_sum'
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[add_monoid M]
[measurable_space M]
[has_measurable_add₂ M]
{μ : measure_theory.measure α}
(l : list (α → M))
(hl : ∀ (f : α → M), f ∈ l → ae_measurable f μ) :
ae_measurable l.sum μ
theorem
list.measurable_prod
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[monoid M]
[measurable_space M]
[has_measurable_mul₂ M]
(l : list (α → M))
(hl : ∀ (f : α → M), f ∈ l → measurable f) :
measurable (λ (x : α), (list.map (λ (f : α → M), f x) l).prod)
theorem
list.measurable_sum
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[add_monoid M]
[measurable_space M]
[has_measurable_add₂ M]
(l : list (α → M))
(hl : ∀ (f : α → M), f ∈ l → measurable f) :
measurable (λ (x : α), (list.map (λ (f : α → M), f x) l).sum)
theorem
list.ae_measurable_prod
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[monoid M]
[measurable_space M]
[has_measurable_mul₂ M]
{μ : measure_theory.measure α}
(l : list (α → M))
(hl : ∀ (f : α → M), f ∈ l → ae_measurable f μ) :
ae_measurable (λ (x : α), (list.map (λ (f : α → M), f x) l).prod) μ
theorem
list.ae_measurable_sum
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[add_monoid M]
[measurable_space M]
[has_measurable_add₂ M]
{μ : measure_theory.measure α}
(l : list (α → M))
(hl : ∀ (f : α → M), f ∈ l → ae_measurable f μ) :
ae_measurable (λ (x : α), (list.map (λ (f : α → M), f x) l).sum) μ
theorem
multiset.measurable_prod'
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[comm_monoid M]
[measurable_space M]
[has_measurable_mul₂ M]
(l : multiset (α → M))
(hl : ∀ (f : α → M), f ∈ l → measurable f) :
theorem
multiset.measurable_sum'
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[add_comm_monoid M]
[measurable_space M]
[has_measurable_add₂ M]
(l : multiset (α → M))
(hl : ∀ (f : α → M), f ∈ l → measurable f) :
theorem
multiset.ae_measurable_prod'
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[comm_monoid M]
[measurable_space M]
[has_measurable_mul₂ M]
{μ : measure_theory.measure α}
(l : multiset (α → M))
(hl : ∀ (f : α → M), f ∈ l → ae_measurable f μ) :
ae_measurable l.prod μ
theorem
multiset.ae_measurable_sum'
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[add_comm_monoid M]
[measurable_space M]
[has_measurable_add₂ M]
{μ : measure_theory.measure α}
(l : multiset (α → M))
(hl : ∀ (f : α → M), f ∈ l → ae_measurable f μ) :
ae_measurable l.sum μ
theorem
multiset.measurable_prod
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[comm_monoid M]
[measurable_space M]
[has_measurable_mul₂ M]
(s : multiset (α → M))
(hs : ∀ (f : α → M), f ∈ s → measurable f) :
measurable (λ (x : α), (multiset.map (λ (f : α → M), f x) s).prod)
theorem
multiset.measurable_sum
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[add_comm_monoid M]
[measurable_space M]
[has_measurable_add₂ M]
(s : multiset (α → M))
(hs : ∀ (f : α → M), f ∈ s → measurable f) :
measurable (λ (x : α), (multiset.map (λ (f : α → M), f x) s).sum)
theorem
multiset.ae_measurable_prod
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[comm_monoid M]
[measurable_space M]
[has_measurable_mul₂ M]
{μ : measure_theory.measure α}
(s : multiset (α → M))
(hs : ∀ (f : α → M), f ∈ s → ae_measurable f μ) :
ae_measurable (λ (x : α), (multiset.map (λ (f : α → M), f x) s).prod) μ
theorem
multiset.ae_measurable_sum
{α : Type u_1}
[measurable_space α]
{M : Type u_2}
[add_comm_monoid M]
[measurable_space M]
[has_measurable_add₂ M]
{μ : measure_theory.measure α}
(s : multiset (α → M))
(hs : ∀ (f : α → M), f ∈ s → ae_measurable f μ) :
ae_measurable (λ (x : α), (multiset.map (λ (f : α → M), f x) s).sum) μ
theorem
finset.measurable_sum'
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
{M : Type u_3}
[add_comm_monoid M]
[measurable_space M]
[has_measurable_add₂ M]
{f : ι → α → M}
(s : finset ι)
(hf : ∀ (i : ι), i ∈ s → measurable (f i)) :
measurable (∑ (i : ι) in s, f i)
theorem
finset.measurable_prod'
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
{M : Type u_3}
[comm_monoid M]
[measurable_space M]
[has_measurable_mul₂ M]
{f : ι → α → M}
(s : finset ι)
(hf : ∀ (i : ι), i ∈ s → measurable (f i)) :
measurable (∏ (i : ι) in s, f i)
theorem
finset.measurable_sum
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
{M : Type u_3}
[add_comm_monoid M]
[measurable_space M]
[has_measurable_add₂ M]
{f : ι → α → M}
(s : finset ι)
(hf : ∀ (i : ι), i ∈ s → measurable (f i)) :
measurable (λ (a : α), ∑ (i : ι) in s, f i a)
theorem
finset.measurable_prod
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
{M : Type u_3}
[comm_monoid M]
[measurable_space M]
[has_measurable_mul₂ M]
{f : ι → α → M}
(s : finset ι)
(hf : ∀ (i : ι), i ∈ s → measurable (f i)) :
measurable (λ (a : α), ∏ (i : ι) in s, f i a)
theorem
finset.ae_measurable_sum'
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
{M : Type u_3}
[add_comm_monoid M]
[measurable_space M]
[has_measurable_add₂ M]
{μ : measure_theory.measure α}
{f : ι → α → M}
(s : finset ι)
(hf : ∀ (i : ι), i ∈ s → ae_measurable (f i) μ) :
ae_measurable (∑ (i : ι) in s, f i) μ
theorem
finset.ae_measurable_prod'
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
{M : Type u_3}
[comm_monoid M]
[measurable_space M]
[has_measurable_mul₂ M]
{μ : measure_theory.measure α}
{f : ι → α → M}
(s : finset ι)
(hf : ∀ (i : ι), i ∈ s → ae_measurable (f i) μ) :
ae_measurable (∏ (i : ι) in s, f i) μ
theorem
finset.ae_measurable_prod
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
{M : Type u_3}
[comm_monoid M]
[measurable_space M]
[has_measurable_mul₂ M]
{f : ι → α → M}
{μ : measure_theory.measure α}
(s : finset ι)
(hf : ∀ (i : ι), i ∈ s → ae_measurable (f i) μ) :
ae_measurable (λ (a : α), ∏ (i : ι) in s, f i a) μ
theorem
finset.ae_measurable_sum
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
{M : Type u_3}
[add_comm_monoid M]
[measurable_space M]
[has_measurable_add₂ M]
{f : ι → α → M}
{μ : measure_theory.measure α}
(s : finset ι)
(hf : ∀ (i : ι), i ∈ s → ae_measurable (f i) μ) :
ae_measurable (λ (a : α), ∑ (i : ι) in s, f i a) μ