mathlib documentation

measure_theory.borel_space

Borel (measurable) space

Main definitions

Main statements

def borel (α : Type u) [topological_space α] :

measurable_space structure generated by topological_space.

Equations
theorem borel_eq_top_of_encodable {α : Type u_1} [topological_space α] [t1_space α] [encodable α] :

theorem borel_comap {α : Type u_1} {β : Type u_2} {f : α → β} {t : topological_space β} :

theorem continuous.borel_measurable {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :

@[class]
structure opens_measurable_space (α : Type u_5) [topological_space α] [h : measurable_space α] :
Prop

A space with measurable_space and topological_space structures such that all open sets are measurable.

Instances
@[class]
structure borel_space (α : Type u_5) [topological_space α] [measurable_space α] :
Prop
  • measurable_eq : _inst_2 = borel α

A space with measurable_space and topological_space structures such that the σ-algebra of measurable sets is exactly the σ-algebra generated by open sets.

Instances
@[instance]

In a borel_space all open sets are measurable.

@[instance]
def subtype.borel_space {α : Type u_1} [topological_space α] [measurable_space α] [hα : borel_space α] (s : set α) :

theorem measurable_of_is_open {γ : Type u_3} {δ : Type u_4} [topological_space γ] [measurable_space γ] [borel_space γ] [measurable_space δ] {f : δ → γ} :
(∀ (s : set γ), is_open sis_measurable (f ⁻¹' s))measurable f

theorem measurable_of_is_closed {γ : Type u_3} {δ : Type u_4} [topological_space γ] [measurable_space γ] [borel_space γ] [measurable_space δ] {f : δ → γ} :
(∀ (s : set γ), is_closed sis_measurable (f ⁻¹' s))measurable f

theorem measurable_of_is_closed' {γ : Type u_3} {δ : Type u_4} [topological_space γ] [measurable_space γ] [borel_space γ] [measurable_space δ] {f : δ → γ} :
(∀ (s : set γ), is_closed ss.nonemptys set.univis_measurable (f ⁻¹' s))measurable f

If s is a measurable set, then 𝓝[s] a is a measurably generated filter for each a. This cannot be an instance because it depends on a non-instance hs : is_measurable s.

theorem is_measurable_le {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [opens_measurable_space α] [measurable_space δ] [partial_order α] [order_closed_topology α] [topological_space.second_countable_topology α] {f g : δ → α} :
measurable fmeasurable gis_measurable {a : δ | f a g a}

theorem is_measurable_lt {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [opens_measurable_space α] [measurable_space δ] [linear_order α] [order_closed_topology α] [topological_space.second_countable_topology α] {f g : δ → α} :
measurable fmeasurable gis_measurable {a : δ | f a < g a}

theorem measurable.max {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [opens_measurable_space α] [measurable_space δ] [decidable_linear_order α] [order_closed_topology α] [topological_space.second_countable_topology α] {f g : δ → α} :
measurable fmeasurable gmeasurable (λ (a : δ), max (f a) (g a))

theorem measurable.min {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [opens_measurable_space α] [measurable_space δ] [decidable_linear_order α] [order_closed_topology α] [topological_space.second_countable_topology α] {f g : δ → α} :
measurable fmeasurable gmeasurable (λ (a : δ), min (f a) (g a))

theorem continuous.measurable {α : Type u_1} {γ : Type u_3} [topological_space α] [measurable_space α] [opens_measurable_space α] [topological_space γ] [measurable_space γ] [borel_space γ] {f : α → γ} :

A continuous function from an opens_measurable_space to a borel_space is measurable.

def homeomorph.to_measurable_equiv {α : Type u_1} {β : Type u_2} [topological_space α] [measurable_space α] [borel_space α] [topological_space β] [measurable_space β] [borel_space β] :
α ≃ₜ βmeasurable_equiv α β

A homeomorphism between two Borel spaces is a measurable equivalence.

Equations
theorem measurable_of_continuous_on_compl_singleton {α : Type u_1} {γ : Type u_3} [topological_space α] [measurable_space α] [opens_measurable_space α] [topological_space γ] [measurable_space γ] [borel_space γ] [t1_space α] {f : α → γ} (a : α) :
continuous_on f {x : α | x a}measurable f

theorem continuous.measurable2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [topological_space α] [measurable_space α] [opens_measurable_space α] [topological_space β] [measurable_space β] [opens_measurable_space β] [topological_space γ] [measurable_space γ] [borel_space γ] [measurable_space δ] [topological_space.second_countable_topology α] [topological_space.second_countable_topology β] {f : δ → α} {g : δ → β} {c : α → β → γ} :
continuous (λ (p : α × β), c p.fst p.snd)measurable fmeasurable gmeasurable (λ (a : δ), c (f a) (g a))

theorem measurable.smul {α : Type u_1} {γ : Type u_3} {δ : Type u_4} [topological_space α] [measurable_space α] [opens_measurable_space α] [topological_space γ] [measurable_space γ] [borel_space γ] [measurable_space δ] [semiring α] [topological_space.second_countable_topology α] [add_comm_monoid γ] [topological_space.second_countable_topology γ] [semimodule α γ] [topological_semimodule α γ] {f : δ → α} {g : δ → γ} :
measurable fmeasurable gmeasurable (λ (c : δ), f c g c)

theorem measurable.const_smul {δ : Type u_4} [measurable_space δ] {R : Type u_1} {M : Type u_2} [topological_space R] [semiring R] [add_comm_monoid M] [semimodule R M] [topological_space M] [topological_semimodule R M] [measurable_space M] [borel_space M] {f : δ → M} (hf : measurable f) (c : R) :
measurable (λ (x : δ), c f x)

theorem measurable_const_smul_iff {γ : Type u_3} {δ : Type u_4} [topological_space γ] [measurable_space γ] [borel_space γ] [measurable_space δ] {α : Type u_1} [topological_space α] [division_ring α] [add_comm_monoid γ] [semimodule α γ] [topological_semimodule α γ] {f : δ → γ} {c : α} :
c 0(measurable (λ (x : δ), c f x) measurable f)

theorem measurable.const_mul {δ : Type u_4} [measurable_space δ] {R : Type u_1} [topological_space R] [measurable_space R] [borel_space R] [semiring R] [topological_semiring R] {f : δ → R} (hf : measurable f) (c : R) :
measurable (λ (x : δ), c * f x)

theorem measurable.mul_const {δ : Type u_4} [measurable_space δ] {R : Type u_1} [topological_space R] [measurable_space R] [borel_space R] [semiring R] [topological_semiring R] {f : δ → R} (hf : measurable f) (c : R) :
measurable (λ (x : δ), (f x) * c)

theorem measurable.add {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [has_add α] [has_continuous_add α] [topological_space.second_countable_topology α] {f g : δ → α} :
measurable fmeasurable gmeasurable (λ (a : δ), f a + g a)

theorem measurable.mul {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [has_mul α] [has_continuous_mul α] [topological_space.second_countable_topology α] {f g : δ → α} :
measurable fmeasurable gmeasurable (λ (a : δ), (f a) * g a)

theorem measurable.add' {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [has_add α] [has_continuous_add α] [topological_space.second_countable_topology α] {f g : δ → α} :
measurable fmeasurable gmeasurable (f + g)

theorem measurable.mul' {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [has_mul α] [has_continuous_mul α] [topological_space.second_countable_topology α] {f g : δ → α} :
measurable fmeasurable gmeasurable (f * g)

A variant of measurable.mul that uses * on functions

theorem measurable_mul_left {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] [has_mul α] [has_continuous_mul α] (x : α) :
measurable (λ (y : α), x * y)

theorem measurable_add_left {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] [has_add α] [has_continuous_add α] (x : α) :
measurable (λ (y : α), x + y)

theorem measurable_mul_right {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] [has_mul α] [has_continuous_mul α] (x : α) :
measurable (λ (y : α), y * x)

theorem measurable_add_right {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] [has_add α] [has_continuous_add α] (x : α) :
measurable (λ (y : α), y + x)

theorem finset.measurable_sum {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] {ι : Type u_2} [add_comm_monoid α] [has_continuous_add α] [topological_space.second_countable_topology α] {f : ι → δ → α} (s : finset ι) :
(∀ (i : ι), measurable (f i))measurable (λ (a : δ), ∑ (i : ι) in s, f i a)

theorem finset.measurable_prod {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] {ι : Type u_2} [comm_monoid α] [has_continuous_mul α] [topological_space.second_countable_topology α] {f : ι → δ → α} (s : finset ι) :
(∀ (i : ι), measurable (f i))measurable (λ (a : δ), ∏ (i : ι) in s, f i a)

theorem measurable.inv {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [group α] [topological_group α] {f : δ → α} :
measurable fmeasurable (λ (a : δ), (f a)⁻¹)

theorem measurable.neg {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [add_group α] [topological_add_group α] {f : δ → α} :
measurable fmeasurable (λ (a : δ), -f a)

theorem measurable.inv' {δ : Type u_4} [measurable_space δ] {α : Type u_1} [normed_field α] [measurable_space α] [borel_space α] {f : δ → α} :
measurable fmeasurable (λ (a : δ), (f a)⁻¹)

theorem measurable.of_neg {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [add_group α] [topological_add_group α] {f : δ → α} :
measurable (λ (a : δ), -f a)measurable f

theorem measurable.of_inv {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [group α] [topological_group α] {f : δ → α} :
measurable (λ (a : δ), (f a)⁻¹)measurable f

@[simp]
theorem measurable_inv_iff {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [group α] [topological_group α] {f : δ → α} :
measurable (λ (a : δ), (f a)⁻¹) measurable f

@[simp]
theorem measurable_neg_iff {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [add_group α] [topological_add_group α] {f : δ → α} :
measurable (λ (a : δ), -f a) measurable f

theorem measurable.sub {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [add_group α] [topological_add_group α] [topological_space.second_countable_topology α] {f g : δ → α} :
measurable fmeasurable gmeasurable (λ (x : δ), f x - g x)

theorem measurable_comp_iff_of_closed_embedding {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [topological_space β] [measurable_space β] [borel_space β] [topological_space γ] [measurable_space γ] [borel_space γ] [measurable_space δ] {f : δ → β} (g : β → γ) :

theorem measurable_of_Iio {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] {f : δ → α} :
(∀ (x : α), is_measurable (f ⁻¹' set.Iio x))measurable f

theorem measurable_of_Ioi {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] {f : δ → α} :
(∀ (x : α), is_measurable (f ⁻¹' set.Ioi x))measurable f

theorem measurable_of_Iic {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] {f : δ → α} :
(∀ (x : α), is_measurable (f ⁻¹' set.Iic x))measurable f

theorem measurable_of_Ici {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] {f : δ → α} :
(∀ (x : α), is_measurable (f ⁻¹' set.Ici x))measurable f

theorem measurable.is_lub {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Type u_2} [encodable ι] {f : ι → δ → α} {g : δ → α} :
(∀ (i : ι), measurable (f i))(∀ (b : δ), is_lub {a : α | ∃ (i : ι), f i b = a} (g b))measurable g

theorem measurable.is_glb {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Type u_2} [encodable ι] {f : ι → δ → α} {g : δ → α} :
(∀ (i : ι), measurable (f i))(∀ (b : δ), is_glb {a : α | ∃ (i : ι), f i b = a} (g b))measurable g

theorem measurable.supr_Prop {δ : Type u_4} [measurable_space δ] {α : Type u_1} [measurable_space α] [complete_lattice α] (p : Prop) {f : δ → α} :
measurable fmeasurable (λ (b : δ), ⨆ (h : p), f b)

theorem measurable.infi_Prop {δ : Type u_4} [measurable_space δ] {α : Type u_1} [measurable_space α] [complete_lattice α] (p : Prop) {f : δ → α} :
measurable fmeasurable (λ (b : δ), ⨅ (h : p), f b)

theorem measurable_supr {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Type u_2} [encodable ι] {f : ι → δ → α} :
(∀ (i : ι), measurable (f i))measurable (λ (b : δ), ⨆ (i : ι), f i b)

theorem measurable_infi {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Type u_2} [encodable ι] {f : ι → δ → α} :
(∀ (i : ι), measurable (f i))measurable (λ (b : δ), ⨅ (i : ι), f i b)

theorem measurable_bsupr {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Type u_2} (s : set ι) {f : ι → δ → α} :
s.countable(∀ (i : ι), measurable (f i))measurable (λ (b : δ), ⨆ (i : ι) (H : i s), f i b)

theorem measurable_binfi {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Type u_2} (s : set ι) {f : ι → δ → α} :
s.countable(∀ (i : ι), measurable (f i))measurable (λ (b : δ), ⨅ (i : ι) (H : i s), f i b)

theorem measurable_liminf' {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Type u_2} {ι' : Type u_3} {f : ι → δ → α} {u : filter ι} (hf : ∀ (i : ι), measurable (f i)) {p : ι' → Prop} {s : ι' → set ι} :
u.has_countable_basis p s(∀ (i : ι'), (s i).countable)measurable (λ (x : δ), u.liminf (λ (i : ι), f i x))

liminf over a general filter is measurable. See measurable_liminf for the version over .

theorem measurable_limsup' {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Type u_2} {ι' : Type u_3} {f : ι → δ → α} {u : filter ι} (hf : ∀ (i : ι), measurable (f i)) {p : ι' → Prop} {s : ι' → set ι} :
u.has_countable_basis p s(∀ (i : ι'), (s i).countable)measurable (λ (x : δ), u.limsup (λ (i : ι), f i x))

limsup over a general filter is measurable. See measurable_limsup for the version over .

theorem measurable_liminf {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {f : δ → α} :
(∀ (i : ), measurable (f i))measurable (λ (x : δ), filter.at_top.liminf (λ (i : ), f i x))

liminf over is measurable. See measurable_liminf' for a version with a general filter.

theorem measurable_limsup {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {f : δ → α} :
(∀ (i : ), measurable (f i))measurable (λ (x : δ), filter.at_top.limsup (λ (i : ), f i x))

limsup over is measurable. See measurable_limsup' for a version with a general filter.

theorem measurable_cSup {α : Type u_1} {δ : Type u_4} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [conditionally_complete_linear_order α] [topological_space.second_countable_topology α] [order_topology α] {ι : Type u_2} {f : ι → δ → α} {s : set ι} :
s.countable(∀ (i : ι), measurable (f i))(∀ (x : δ), bdd_above ((λ (i : ι), f i x) '' s))measurable (λ (x : δ), Sup ((λ (i : ι), f i x) '' s))

@[instance]

@[instance]

@[instance]

@[instance]

@[instance]

@[instance]

theorem is_measurable_ball {α : Type u_1} [metric_space α] [measurable_space α] [opens_measurable_space α] {x : α} {ε : } :

theorem measurable_inf_dist {α : Type u_1} [metric_space α] [measurable_space α] [opens_measurable_space α] {s : set α} :
measurable (λ (x : α), metric.inf_dist x s)

theorem measurable.inf_dist {α : Type u_1} {β : Type u_2} [metric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] {f : β → α} (hf : measurable f) {s : set α} :
measurable (λ (x : β), metric.inf_dist (f x) s)

theorem measurable_inf_nndist {α : Type u_1} [metric_space α] [measurable_space α] [opens_measurable_space α] {s : set α} :
measurable (λ (x : α), metric.inf_nndist x s)

theorem measurable.inf_nndist {α : Type u_1} {β : Type u_2} [metric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] {f : β → α} (hf : measurable f) {s : set α} :
measurable (λ (x : β), metric.inf_nndist (f x) s)

theorem measurable.dist {α : Type u_1} {β : Type u_2} [metric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] [topological_space.second_countable_topology α] {f g : β → α} :
measurable fmeasurable gmeasurable (λ (b : β), dist (f b) (g b))

theorem measurable.nndist {α : Type u_1} {β : Type u_2} [metric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] [topological_space.second_countable_topology α] {f g : β → α} :
measurable fmeasurable gmeasurable (λ (b : β), nndist (f b) (g b))

theorem is_measurable_eball {α : Type u_1} [emetric_space α] [measurable_space α] [opens_measurable_space α] {x : α} {ε : ennreal} :

theorem measurable_edist_right {α : Type u_1} [emetric_space α] [measurable_space α] [opens_measurable_space α] {x : α} :

theorem measurable_edist_left {α : Type u_1} [emetric_space α] [measurable_space α] [opens_measurable_space α] {x : α} :
measurable (λ (y : α), edist y x)

theorem measurable_inf_edist {α : Type u_1} [emetric_space α] [measurable_space α] [opens_measurable_space α] {s : set α} :
measurable (λ (x : α), emetric.inf_edist x s)

theorem measurable.inf_edist {α : Type u_1} {β : Type u_2} [emetric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] {f : β → α} (hf : measurable f) {s : set α} :
measurable (λ (x : β), emetric.inf_edist (f x) s)

theorem measurable.edist {α : Type u_1} {β : Type u_2} [emetric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] [topological_space.second_countable_topology α] {f g : β → α} :
measurable fmeasurable gmeasurable (λ (b : β), edist (f b) (g b))

theorem measurable.sub_nnreal {α : Type u_1} [measurable_space α] {f g : α → ℝ≥0} :
measurable fmeasurable gmeasurable (λ (a : α), f a - g a)

theorem measurable.nnreal_of_real {α : Type u_1} [measurable_space α] {f : α → } :
measurable fmeasurable (λ (x : α), nnreal.of_real (f x))

theorem measurable.nnreal_coe {α : Type u_1} [measurable_space α] {f : α → ℝ≥0} :
measurable fmeasurable (λ (x : α), (f x))

theorem measurable.ennreal_coe {α : Type u_1} [measurable_space α] {f : α → ℝ≥0} :
measurable fmeasurable (λ (x : α), (f x))

theorem measurable.ennreal_of_real {α : Type u_1} [measurable_space α] {f : α → } :
measurable fmeasurable (λ (x : α), ennreal.of_real (f x))

theorem ennreal.measurable_of_measurable_nnreal {α : Type u_1} [measurable_space α] {f : ennreal → α} :
measurable (λ (p : ℝ≥0), f p)measurable f

ennreal is measurable_equiv to ℝ≥0 ⊕ unit.

Equations
theorem ennreal.measurable_of_measurable_nnreal_prod {β : Type u_2} {γ : Type u_3} [measurable_space β] [measurable_space γ] {f : ennreal × β → γ} :
measurable (λ (p : ℝ≥0 × β), f ((p.fst), p.snd))measurable (λ (x : β), f (, x))measurable f

theorem ennreal.measurable_of_measurable_nnreal_nnreal {β : Type u_2} [measurable_space β] {f : ennreal × ennreal → β} :
measurable (λ (p : ℝ≥0 × ℝ≥0), f ((p.fst), (p.snd)))measurable (λ (r : ℝ≥0), f (, r))measurable (λ (r : ℝ≥0), f (r, ))measurable f

theorem measurable.to_nnreal {α : Type u_1} [measurable_space α] {f : α → ennreal} :
measurable fmeasurable (λ (x : α), (f x).to_nnreal)

theorem measurable_ennreal_coe_iff {α : Type u_1} [measurable_space α] {f : α → ℝ≥0} :
measurable (λ (x : α), (f x)) measurable f

theorem measurable.to_real {α : Type u_1} [measurable_space α] {f : α → ennreal} :
measurable fmeasurable (λ (x : α), (f x).to_real)

theorem measurable.ennreal_mul {α : Type u_1} [measurable_space α] {f g : α → ennreal} :
measurable fmeasurable gmeasurable (λ (a : α), (f a) * g a)

theorem measurable.ennreal_add {α : Type u_1} [measurable_space α] {f g : α → ennreal} :
measurable fmeasurable gmeasurable (λ (a : α), f a + g a)

theorem measurable.ennreal_sub {α : Type u_1} [measurable_space α] {f g : α → ennreal} :
measurable fmeasurable gmeasurable (λ (a : α), f a - g a)

theorem measurable.ennreal_tsum {α : Type u_1} [measurable_space α] {ι : Type u_2} [encodable ι] {f : ι → α → ennreal} :
(∀ (i : ι), measurable (f i))measurable (λ (x : α), ∑' (i : ι), f i x)

note: ennreal can probably be generalized in a future version of this lemma.

theorem measurable.norm {α : Type u_1} {β : Type u_2} [measurable_space α] [normed_group α] [opens_measurable_space α] [measurable_space β] {f : β → α} :
measurable fmeasurable (λ (a : β), f a)

theorem measurable.nnnorm {α : Type u_1} {β : Type u_2} [measurable_space α] [normed_group α] [opens_measurable_space α] [measurable_space β] {f : β → α} :
measurable fmeasurable (λ (a : β), nnnorm (f a))

theorem measurable_ennnorm {α : Type u_1} [measurable_space α] [normed_group α] [opens_measurable_space α] :
measurable (λ (x : α), (nnnorm x))

theorem measurable.ennnorm {α : Type u_1} {β : Type u_2} [measurable_space α] [normed_group α] [opens_measurable_space α] [measurable_space β] {f : β → α} :
measurable fmeasurable (λ (a : β), (nnnorm (f a)))

theorem measurable_of_tendsto_nnreal' {α : Type u_1} [measurable_space α] {ι : Type u_2} {ι' : Type u_3} {f : ι → α → ℝ≥0} {g : α → ℝ≥0} (u : filter ι) [u.ne_bot] (hf : ∀ (i : ι), measurable (f i)) (lim : filter.tendsto f u (𝓝 g)) {p : ι' → Prop} {s : ι' → set ι} :
u.has_countable_basis p s(∀ (i : ι'), (s i).countable)measurable g

A limit (over a general filter) of measurable ℝ≥0 valued functions is measurable. The assumption hs can be dropped using filter.is_countably_generated.has_antimono_basis, but we don't need that case yet.

theorem measurable_of_tendsto_nnreal {α : Type u_1} [measurable_space α] {f : α → ℝ≥0} {g : α → ℝ≥0} :
(∀ (i : ), measurable (f i))filter.tendsto f filter.at_top (𝓝 g)measurable g

A sequential limit of measurable ℝ≥0 valued functions is measurable.

theorem measurable_of_tendsto_metric' {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] [metric_space β] [borel_space β] {ι : Type u_3} {ι' : Type u_4} {f : ι → α → β} {g : α → β} (u : filter ι) [u.ne_bot] (hf : ∀ (i : ι), measurable (f i)) (lim : filter.tendsto f u (𝓝 g)) {p : ι' → Prop} {s : ι' → set ι} :
u.has_countable_basis p s(∀ (i : ι'), (s i).countable)measurable g

A limit (over a general filter) of measurable functions valued in a metric space is measurable. The assumption hs can be dropped using filter.is_countably_generated.has_antimono_basis, but we don't need that case yet.

theorem measurable_of_tendsto_metric {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] [metric_space β] [borel_space β] {f : α → β} {g : α → β} :
(∀ (i : ), measurable (f i))filter.tendsto f filter.at_top (𝓝 g)measurable g

A sequential limit of measurable functions valued in a metric space is measurable.

theorem continuous_linear_map.measurable {𝕜 : Type u_5} [normed_field 𝕜] {E : Type u_6} [normed_group E] [normed_space 𝕜 E] [measurable_space E] [opens_measurable_space E] {F : Type u_7} [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F] (L : E →L[𝕜] F) :

theorem continuous_linear_map.measurable_comp {α : Type u_1} [measurable_space α] {𝕜 : Type u_5} [normed_field 𝕜] {E : Type u_6} [normed_group E] [normed_space 𝕜 E] [measurable_space E] [opens_measurable_space E] {F : Type u_7} [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F] (L : E →L[𝕜] F) {φ : α → E} :
measurable φmeasurable (λ (a : α), L (φ a))

theorem measurable_smul_const {α : Type u_1} [measurable_space α] {𝕜 : Type u_5} [nondiscrete_normed_field 𝕜] [complete_space 𝕜] [measurable_space 𝕜] [borel_space 𝕜] {E : Type u_6} [normed_group E] [normed_space 𝕜 E] [measurable_space E] [borel_space E] {f : α → 𝕜} {c : E} :
c 0(measurable (λ (x : α), f x c) measurable f)

A measure μ is regular if

  • it is finite on all compact sets;
  • it is outer regular: μ(A) = inf { μ(U) | A ⊆ U open } for A measurable;
  • it is inner regular: μ(U) = sup { μ(K) | K ⊆ U compact } for U open.
theorem measure_theory.measure.regular.outer_regular_eq {α : Type u_1} [measurable_space α] [topological_space α] {μ : measure_theory.measure α} (hμ : μ.regular) ⦃A : set α⦄ :
is_measurable A(⨅ (U : set α) (h : is_open U) (h2 : A U), μ U) = μ A

theorem measure_theory.measure.regular.inner_regular_eq {α : Type u_1} [measurable_space α] [topological_space α] {μ : measure_theory.measure α} (hμ : μ.regular) ⦃U : set α⦄ :
is_open U(⨆ (K : set α) (h : is_compact K) (h2 : K U), μ K) = μ U

theorem measure_theory.measure.regular.smul {α : Type u_1} [measurable_space α] [topological_space α] {μ : measure_theory.measure α} (hμ : μ.regular) {x : ennreal} :
x < (x μ).regular