# mathlibdocumentation

measure_theory.​borel_space

# Borel (measurable) space

## Main definitions

• borel α : the least σ-algebra that contains all open sets;
• class borel_space : a space with topological_space and measurable_space structures such that ‹measurable_space α› = borel α;
• class opens_measurable_space : a space with topological_space and measurable_space structures such that all open sets are measurable; equivalently, borel α ≤ ‹measurable_space α›.
• borel_space instances on empty, unit, bool, nat, int, rat;
• measurable and borel_space instances on ℝ, ℝ≥0, ennreal.
• A measure is regular if it is finite on compact sets, inner regular and outer regular.

## Main statements

• is_open.is_measurable, is_closed.is_measurable: open and closed sets are measurable;
• continuous.measurable : a continuous function is measurable;
• continuous.measurable2 : if f : α → β and g : α → γ are measurable and op : β × γ → δ is continuous, then λ x, op (f x, g y) is measurable;
• measurable.add etc : dot notation for arithmetic operations on measurable predicates, and similarly for dist and edist;
• measurable.ennreal* : special cases for arithmetic operations on ennreals.
def borel (α : Type u) :

measurable_space structure generated by topological_space.

Equations
theorem borel_eq_top_of_discrete {α : Type u} :

theorem borel_eq_top_of_encodable {α : Type u} [t1_space α] [encodable α] :

theorem borel_eq_generate_from_of_subbasis {α : Type u} {s : set (set α)} [t : topological_space α] :

theorem borel_eq_generate_Iio (α : Type u_1) [linear_order α] :

theorem borel_eq_generate_Ioi (α : Type u_1) [linear_order α] :

theorem borel_comap {α : Type u} {β : Type v} {f : α → β} {t : topological_space β} :

theorem continuous.​borel_measurable {α : Type u} {β : Type v} {f : α → β} :

@[class]
structure opens_measurable_space (α : Type u_1) [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_1) :
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]
def borel_space.​opens_measurable {α : Type u_1} [borel_space α] :

In a borel_space all open sets are measurable.

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

Equations
• _ = _
@[instance]
def subtype.​opens_measurable_space {α : Type u_1} [h : opens_measurable_space α] (s : set α) :

Equations
• _ = _
theorem is_open.​is_measurable {α : Type u} {s : set α} :

theorem is_measurable_interior {α : Type u} {s : set α} :

theorem is_closed.​is_measurable {α : Type u} {s : set α} :

theorem is_compact.​is_measurable {α : Type u} {s : set α} [t2_space α] :

theorem is_measurable_closure {α : Type u} {s : set α} :

@[instance]
def nhds_is_measurably_generated {α : Type u} (a : α) :

Equations
• _ = _
theorem is_measurable.​nhds_within_is_measurably_generated {α : Type u} {s : set α} (hs : is_measurable s) (a : α) :

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.

@[instance]

Equations
theorem is_measurable_Ici {α : Type u} [preorder α] {a : α} :

theorem is_measurable_Iic {α : Type u} [preorder α] {a : α} :

theorem is_measurable_Icc {α : Type u} [preorder α] {a b : α} :

@[instance]

Equations
@[instance]

Equations
theorem is_measurable_Iio {α : Type u} [linear_order α] {a : α} :

theorem is_measurable_Ioi {α : Type u} [linear_order α] {a : α} :

theorem is_measurable_Ioo {α : Type u} [linear_order α] {a b : α} :

theorem is_measurable_Ioc {α : Type u} [linear_order α] {a b : α} :

theorem is_measurable_Ico {α : Type u} [linear_order α] {a b : α} :

theorem is_measurable_interval {α : Type u} {a b : α} :

@[instance]
def prod.​opens_measurable_space {α : Type u} {β : Type v} :

Equations
theorem continuous.​measurable {α : Type u} {γ : Type w} [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} [borel_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} {γ : Type w} [borel_space γ] [t1_space α] {f : α → γ} (a : α) :
continuous_on f {x : α | x a} → measurable f

theorem continuous.​measurable2 {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [borel_space γ] {f : δ → α} {g : δ → β} {c : α → β → γ} :
continuous (λ (p : α × β), c p.fst p.snd) → measurable f → measurable g → measurable (λ (a : δ), c (f a) (g a))

theorem measurable.​smul {α : Type u} {γ : Type w} {δ : Type x} [borel_space γ] [semiring α] [semimodule α γ] {f : δ → α} {g : δ → γ} :
measurable f → measurable g → measurable (λ (c : δ), f c g c)

theorem measurable.​const_smul {γ : Type w} {δ : Type x} [borel_space γ] {α : Type u_1} [semiring α] [semimodule α γ] {f : δ → γ} (hf : measurable f) (c : α) :
measurable (λ (x : δ), c f x)

theorem measurable_const_smul_iff {γ : Type w} {δ : Type x} [borel_space γ] {α : Type u_1} [semimodule α γ] {f : δ → γ} {c : α} :
c 0 → (measurable (λ (x : δ), c f x) measurable f)

theorem is_measurable_le' {α : Type u} :
is_measurable {p : α × α | p.fst p.snd}

theorem is_measurable_le {α : Type u} {δ : Type x} {f g : δ → α} :
measurable f → measurable g → is_measurable {a : δ | f a g a}

theorem measurable.​max {α : Type u} {δ : Type x} {f g : δ → α} :
measurable f → measurable g → measurable (λ (a : δ), max (f a) (g a))

theorem measurable.​min {α : Type u} {δ : Type x} {f g : δ → α} :
measurable f → measurable g → measurable (λ (a : δ), min (f a) (g a))

theorem prod_le_borel_prod {α : Type u} {β : Type v} [borel_space α] [borel_space β] :

@[instance]
def prod.​borel_space {α : Type u} {β : Type v} [borel_space α] [borel_space β] :
borel_space× β)

Equations
measurable (λ (p : α × α), p.fst + p.snd)

theorem measurable_mul {α : Type u} [borel_space α] [has_mul α] :
measurable (λ (p : α × α), p.fst * p.snd)

theorem measurable.​add {α : Type u} {δ : Type x} [borel_space α] [has_add α] {f g : δ → α} :
measurable f → measurable g → measurable (λ (a : δ), f a + g a)

theorem measurable.​mul {α : Type u} {δ : Type x} [borel_space α] [has_mul α] {f g : δ → α} :
measurable f → measurable g → measurable (λ (a : δ), f a * g a)

theorem measurable_mul_left {α : Type u} [borel_space α] [has_mul α] (x : α) :
measurable (λ (y : α), x * y)

theorem measurable_add_left {α : Type u} [borel_space α] [has_add α] (x : α) :
measurable (λ (y : α), x + y)

theorem measurable_mul_right {α : Type u} [borel_space α] [has_mul α] (x : α) :
measurable (λ (y : α), y * x)

theorem measurable_add_right {α : Type u} [borel_space α] [has_add α] (x : α) :
measurable (λ (y : α), y + x)

theorem finset.​measurable_sum {α : Type u} {δ : Type x} [borel_space α] {ι : Type u_1} {f : ι → δ → α} (s : finset ι) :
(∀ (i : ι), measurable (f i)) → measurable (λ (a : δ), s.sum (λ (i : ι), f i a))

theorem finset.​measurable_prod {α : Type u} {δ : Type x} [borel_space α] {ι : Type u_1} [comm_monoid α] {f : ι → δ → α} (s : finset ι) :
(∀ (i : ι), measurable (f i)) → measurable (λ (a : δ), s.prod (λ (i : ι), f i a))

theorem measurable_inv {α : Type u} [borel_space α] [group α] :

theorem measurable_neg {α : Type u} [borel_space α] [add_group α] :

theorem measurable.​inv {α : Type u} {δ : Type x} [borel_space α] [group α] {f : δ → α} :
measurable f → measurable (λ (a : δ), (f a)⁻¹)

theorem measurable.​neg {α : Type u} {δ : Type x} [borel_space α] [add_group α] {f : δ → α} :
measurable f → measurable (λ (a : δ), -f a)

theorem measurable_inv' {α : Type u_1} [normed_field α] [borel_space α] :

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

theorem measurable.​of_inv {α : Type u} {δ : Type x} [borel_space α] [group α] {f : δ → α} :
measurable (λ (a : δ), (f a)⁻¹) → measurable f

theorem measurable.​of_neg {α : Type u} {δ : Type x} [borel_space α] [add_group α] {f : δ → α} :
measurable (λ (a : δ), -f a) → measurable f

@[simp]
theorem measurable_inv_iff {α : Type u} {δ : Type x} [borel_space α] [group α] {f : δ → α} :
measurable (λ (a : δ), (f a)⁻¹) measurable f

@[simp]
theorem measurable_neg_iff {α : Type u} {δ : Type x} [borel_space α] [add_group α] {f : δ → α} :
measurable (λ (a : δ), -f a) measurable f

theorem measurable.​sub {α : Type u} {δ : Type x} [borel_space α] [add_group α] {f g : δ → α} :
measurable f → measurable g → measurable (λ (x : δ), f x - g x)

theorem measurable.​is_lub {α : Type u} {δ : Type x} [borel_space α] [linear_order α] {ι : Type u_1} [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} {δ : Type x} [borel_space α] [linear_order α] {ι : Type u_1} [encodable ι] {f : ι → δ → α} {g : δ → α} :
(∀ (i : ι), measurable (f i)) → (∀ (b : δ), is_glb {a : α | ∃ (i : ι), f i b = a} (g b)) → measurable g

theorem measurable_supr {α : Type u} {δ : Type x} [borel_space α] {ι : Type u_1} [encodable ι] {f : ι → δ → α} :
(∀ (i : ι), measurable (f i)) → measurable (λ (b : δ), ⨆ (i : ι), f i b)

theorem measurable_infi {α : Type u} {δ : Type x} [borel_space α] {ι : Type u_1} [encodable ι] {f : ι → δ → α} :
(∀ (i : ι), measurable (f i)) → measurable (λ (b : δ), ⨅ (i : ι), f i b)

theorem measurable.​supr_Prop {δ : Type x} {α : Type u_1} (p : Prop) {f : δ → α} :
measurable f → measurable (λ (b : δ), ⨆ (h : p), f b)

theorem measurable.​infi_Prop {δ : Type x} {α : Type u_1} (p : Prop) {f : δ → α} :
measurable f → measurable (λ (b : δ), ⨅ (h : p), f b)

theorem measurable_bsupr {α : Type u} {δ : Type x} [borel_space α] {ι : Type u_1} [encodable ι] (p : ι → Prop) {f : ι → δ → α} :
(∀ (i : ι), measurable (f i)) → measurable (λ (b : δ), ⨆ (i : ι) (hi : p i), f i b)

theorem measurable_binfi {α : Type u} {δ : Type x} [borel_space α] {ι : Type u_1} [encodable ι] (p : ι → Prop) {f : ι → δ → α} :
(∀ (i : ι), measurable (f i)) → measurable (λ (b : δ), ⨅ (i : ι) (hi : p i), f i b)

def homemorph.​to_measurable_equiv {α : Type u} {β : Type v} [borel_space α] [borel_space β] :
α ≃ₜ β → measurable_equiv α β

Convert a homeomorph to a measurable_equiv.

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
theorem is_measurable_ball {α : Type u} [metric_space α] {x : α} {ε : } :

theorem is_measurable_closed_ball {α : Type u} [metric_space α] {x : α} {ε : } :

theorem measurable_dist {α : Type u} [metric_space α] :
measurable (λ (p : α × α), has_dist.dist p.fst p.snd)

theorem measurable.​dist {α : Type u} {β : Type v} [metric_space α] {f g : β → α} :
measurable f → measurable g → measurable (λ (b : β), has_dist.dist (f b) (g b))

theorem measurable_nndist {α : Type u} [metric_space α] :
measurable (λ (p : α × α), nndist p.fst p.snd)

theorem measurable.​nndist {α : Type u} {β : Type v} [metric_space α] {f g : β → α} :
measurable f → measurable g → measurable (λ (b : β), nndist (f b) (g b))

theorem is_measurable_eball {α : Type u} {x : α} {ε : ennreal} :

theorem measurable_edist {α : Type u} :
measurable (λ (p : α × α), has_edist.edist p.fst p.snd)

theorem measurable.​edist {α : Type u} {β : Type v} {f g : β → α} :
measurable f → measurable g → measurable (λ (b : β), has_edist.edist (f b) (g b))

theorem measurable.​sub_nnreal {α : Type u} {f g : α → nnreal} :
measurable f → measurable g → measurable (λ (a : α), f a - g a)

theorem measurable.​nnreal_of_real {α : Type u} {f : α → } :
measurable f → measurable (λ (x : α), nnreal.of_real (f x))

theorem measurable.​nnreal_coe {α : Type u} {f : α → nnreal} :
measurable f → measurable (λ (x : α), (f x))

theorem measurable.​ennreal_coe {α : Type u} {f : α → nnreal} :
measurable f → measurable (λ (x : α), (f x))

theorem measurable.​ennreal_of_real {α : Type u} {f : α → } :
measurable f → measurable (λ (x : α), ennreal.of_real (f x))

The set of finite ennreal numbers is measurable_equiv to nnreal.

Equations
theorem ennreal.​measurable_of_measurable_nnreal {α : Type u} {f : ennreal → α} :
measurable (λ (p : nnreal), f p) → measurable f

ennreal is measurable_equiv to nnreal ⊕ unit.

Equations
theorem ennreal.​measurable_of_measurable_nnreal_nnreal {α : Type u} {β : Type v} (f : ennrealennreal → β) {g h : α → ennreal} :
measurable (λ (p : nnreal × nnreal), f (p.fst) (p.snd)) → measurable (λ (r : nnreal), f r) → measurable (λ (r : nnreal), f r ) → measurable g → measurable h → measurable (λ (a : α), f (g a) (h a))

theorem measurable.​ennreal_mul {α : Type u_1} {f g : α → ennreal} :
measurable f → measurable g → measurable (λ (a : α), f a * g a)

theorem measurable.​ennreal_add {α : Type u_1} {f g : α → ennreal} :
measurable f → measurable g → measurable (λ (a : α), f a + g a)

theorem measurable.​ennreal_sub {α : Type u_1} {f g : α → ennreal} :
measurable f → measurable g → measurable (λ (a : α), f a - g a)

theorem measurable_norm {α : Type u} [normed_group α] :

theorem measurable.​norm {α : Type u} {β : Type v} [normed_group α] {f : β → α} :
measurable f → measurable (λ (a : β), f a)

theorem measurable_nnnorm {α : Type u} [normed_group α] :

theorem measurable.​nnnorm {α : Type u} {β : Type v} [normed_group α] {f : β → α} :
measurable f → measurable (λ (a : β), nnnorm (f a))

theorem measurable.​ennnorm {α : Type u} {β : Type v} [normed_group α] {f : β → α} :
measurable f → measurable (λ (a : β), (nnnorm (f a)))

structure measure_theory.​measure.​regular {α : Type u} :

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} {μ : 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} {μ : 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.​map {α : Type u} {β : Type v} [t2_space β] [borel_space β] {μ : measure_theory.measure α} (hμ : μ.regular) (f : α ≃ₜ β) :

theorem measure_theory.​measure.​regular.​smul {α : Type u} {μ : measure_theory.measure α} (hμ : μ.regular) {x : ennreal} :
x < → (x μ).regular