# 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, ℝ≥0∞.
• A measure is regular if it is finite on compact sets, inner regular and outer regular.

## Main statements #

• is_open.measurable_set, is_closed.measurable_set: 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;
• ae_measurable.add : similar dot notation for almost everywhere measurable functions;
• measurable.ennreal* : special cases for arithmetic operations on ℝ≥0∞.
def borel (α : Type u)  :

measurable_space structure generated by topological_space.

Equations
theorem borel_eq_top_of_discrete {α : Type u_1}  :
theorem borel_eq_top_of_encodable {α : Type u_1} [t1_space α] [encodable α] :
theorem borel_eq_generate_from_of_subbasis {α : Type u_1} {s : set (set α)} [t : topological_space α] (hs : t = ) :
theorem is_pi_system_is_open {α : Type u_1}  :
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_1} {β : Type u_2} {f : α → β} {t : topological_space β} :
=
theorem continuous.borel_measurable {α : Type u_1} {β : Type u_2} {f : α → β} (hf : continuous f) :
@[class]
structure opens_measurable_space (α : Type u_6) [h : measurable_space α] :
Prop
• borel_le : h

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

Instances
@[class]
structure borel_space (α : Type u_6)  :
Prop
• measurable_eq : _inst_2 =

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
@[protected, instance]
def borel_space.opens_measurable {α : Type u_1} [borel_space α] :

In a borel_space all open sets are measurable.

@[protected, instance]
def subtype.borel_space {α : Type u_1} [hα : borel_space α] (s : set α) :
@[protected, instance]
def subtype.opens_measurable_space {α : Type u_1} [h : opens_measurable_space α] (s : set α) :
theorem is_open.measurable_set {α : Type u_1} {s : set α} (h : is_open s) :
theorem measurable_set_interior {α : Type u_1} {s : set α}  :
theorem is_Gδ.measurable_set {α : Type u_1} {s : set α} (h : is_Gδ s) :
theorem measurable_set_of_continuous_at {α : Type u_1} {β : Type u_2} (f : α → β) :
measurable_set {x : α | x}
theorem is_closed.measurable_set {α : Type u_1} {s : set α} (h : is_closed s) :
theorem is_compact.measurable_set {α : Type u_1} {s : set α} [t2_space α] (h : is_compact s) :
theorem measurable_set_closure {α : Type u_1} {s : set α}  :
theorem measurable_of_is_open {γ : Type u_3} {δ : Type u_5} [borel_space γ] {f : δ → γ} (hf : ∀ (s : set γ), measurable_set (f ⁻¹' s)) :
theorem measurable_of_is_closed {γ : Type u_3} {δ : Type u_5} [borel_space γ] {f : δ → γ} (hf : ∀ (s : set γ), measurable_set (f ⁻¹' s)) :
theorem measurable_of_is_closed' {γ : Type u_3} {δ : Type u_5} [borel_space γ] {f : δ → γ} (hf : ∀ (s : set γ), s.nonemptymeasurable_set (f ⁻¹' s)) :
@[protected, instance]
def nhds_is_measurably_generated {α : Type u_1} (a : α) :
theorem measurable_set.nhds_within_is_measurably_generated {α : Type u_1} {s : set α} (hs : measurable_set 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 : measurable_set s.

@[protected, instance]
@[protected, instance]
def pi.opens_measurable_space {ι : Type u_1} {π : ι → Type u_2} [fintype ι] [t' : Π (i : ι), topological_space («π» i)] [Π (i : ι), measurable_space («π» i)] [∀ (i : ι), ] [∀ (i : ι), opens_measurable_space («π» i)] :
opens_measurable_space (Π (i : ι), «π» i)
@[protected, instance]
def prod.opens_measurable_space {α : Type u_1} {β : Type u_2}  :
@[simp]
theorem measurable_set_Ici {α : Type u_1} [preorder α] {a : α} :
@[simp]
theorem measurable_set_Iic {α : Type u_1} [preorder α] {a : α} :
@[simp]
theorem measurable_set_Icc {α : Type u_1} [preorder α] {a b : α} :
@[protected, instance]
def nhds_within_Ici_is_measurably_generated {α : Type u_1} [preorder α] {a b : α} :
@[protected, instance]
def nhds_within_Iic_is_measurably_generated {α : Type u_1} [preorder α] {a b : α} :
@[protected, instance]
def at_top_is_measurably_generated {α : Type u_1} [preorder α]  :
@[protected, instance]
def at_bot_is_measurably_generated {α : Type u_1} [preorder α]  :
theorem measurable_set_le' {α : Type u_1}  :
measurable_set {p : α × α | p.fst p.snd}
theorem measurable_set_le {α : Type u_1} {δ : Type u_5} {f g : δ → α} (hf : measurable f) (hg : measurable g) :
measurable_set {a : δ | f a g a}
@[simp]
theorem measurable_set_Iio {α : Type u_1} [linear_order α] {a : α} :
@[simp]
theorem measurable_set_Ioi {α : Type u_1} [linear_order α] {a : α} :
@[simp]
theorem measurable_set_Ioo {α : Type u_1} [linear_order α] {a b : α} :
@[simp]
theorem measurable_set_Ioc {α : Type u_1} [linear_order α] {a b : α} :
@[simp]
theorem measurable_set_Ico {α : Type u_1} [linear_order α] {a b : α} :
@[protected, instance]
def nhds_within_Ioi_is_measurably_generated {α : Type u_1} [linear_order α] {a b : α} :
@[protected, instance]
def nhds_within_Iio_is_measurably_generated {α : Type u_1} [linear_order α] {a b : α} :
theorem measurable_set_lt' {α : Type u_1} [linear_order α]  :
measurable_set {p : α × α | p.fst < p.snd}
theorem measurable_set_lt {α : Type u_1} {δ : Type u_5} [linear_order α] {f g : δ → α} (hf : measurable f) (hg : measurable g) :
measurable_set {a : δ | f a < g a}
theorem measurable_set_interval {α : Type u_1} [linear_order α] {a b : α} :
theorem measurable.max {α : Type u_1} {δ : Type u_5} [linear_order α] {f g : δ → α} (hf : measurable f) (hg : measurable g) :
measurable (λ (a : δ), max (f a) (g a))
theorem ae_measurable.max {α : Type u_1} {δ : Type u_5} [linear_order α] {f g : δ → α} {μ : measure_theory.measure δ} (hf : μ) (hg : μ) :
ae_measurable (λ (a : δ), max (f a) (g a)) μ
theorem measurable.min {α : Type u_1} {δ : Type u_5} [linear_order α] {f g : δ → α} (hf : measurable f) (hg : measurable g) :
measurable (λ (a : δ), min (f a) (g a))
theorem ae_measurable.min {α : Type u_1} {δ : Type u_5} [linear_order α] {f g : δ → α} {μ : measure_theory.measure δ} (hf : μ) (hg : μ) :
ae_measurable (λ (a : δ), min (f a) (g a)) μ
theorem continuous.measurable {α : Type u_1} {γ : Type u_3} [borel_space γ] {f : α → γ} (hf : continuous f) :

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

theorem continuous.ae_measurable {α : Type u_1} {γ : Type u_3} [borel_space γ] {f : α → γ} (h : continuous f) (μ : measure_theory.measure α) :

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

theorem closed_embedding.measurable {α : Type u_1} {γ : Type u_3} [borel_space γ] {f : α → γ} (hf : closed_embedding f) :
@[protected, instance]
@[protected, instance]
def has_continuous_mul.has_measurable_mul {γ : Type u_3} [borel_space γ] [has_mul γ]  :
@[protected, instance]
def has_continuous_sub.has_measurable_sub {γ : Type u_3} [borel_space γ] [has_sub γ]  :
@[protected, instance]
@[protected, instance]
def topological_group.has_measurable_inv {γ : Type u_3} [borel_space γ] [group γ]  :
@[protected, instance]
def has_continuous_smul.has_measurable_smul {M : Type u_1} {α : Type u_2} [borel_space α] [ α] [ α] :
def homeomorph.to_measurable_equiv {γ : Type u_3} {γ₂ : Type u_4} [borel_space γ] [measurable_space γ₂] [borel_space γ₂] (h : γ ≃ₜ γ₂) :
γ ≃ᵐ γ₂

A homeomorphism between two Borel spaces is a measurable equivalence.

Equations
@[simp]
theorem homeomorph.to_measurable_equiv_coe {γ : Type u_3} {γ₂ : Type u_4} [borel_space γ] [measurable_space γ₂] [borel_space γ₂] (h : γ ≃ₜ γ₂) :
@[simp]
theorem homeomorph.to_measurable_equiv_symm_coe {γ : Type u_3} {γ₂ : Type u_4} [borel_space γ] [measurable_space γ₂] [borel_space γ₂] (h : γ ≃ₜ γ₂) :
theorem homeomorph.measurable {α : Type u_1} {γ : Type u_3} [borel_space γ] (h : α ≃ₜ γ) :
theorem measurable_of_continuous_on_compl_singleton {α : Type u_1} {γ : Type u_3} [borel_space γ] [t1_space α] {f : α → γ} (a : α) (hf : {a}) :
theorem continuous.measurable2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [borel_space γ] {f : δ → α} {g : δ → β} {c : α → β → γ} (h : continuous (λ (p : α × β), c p.fst p.snd)) (hf : measurable f) (hg : measurable g) :
measurable (λ (a : δ), c (f a) (g a))
theorem continuous.ae_measurable2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [borel_space γ] {f : δ → α} {g : δ → β} {c : α → β → γ} {μ : measure_theory.measure δ} (h : continuous (λ (p : α × β), c p.fst p.snd)) (hf : μ) (hg : μ) :
ae_measurable (λ (a : δ), c (f a) (g a)) μ
@[protected, instance]
def has_continuous_inv'.has_measurable_inv {γ : Type u_3} [borel_space γ] [t1_space γ]  :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def has_continuous_smul.has_measurable_smul₂ {M : Type u_1} {α : Type u_2} [borel_space α] [ α] [ α] :
theorem pi_le_borel_pi {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space («π» i)] [Π (i : ι), measurable_space («π» i)] [∀ (i : ι), borel_space («π» i)] :
measurable_space.pi borel (Π (i : ι), «π» i)
theorem prod_le_borel_prod {α : Type u_1} {β : Type u_2} [borel_space α] [borel_space β] :
@[protected, instance]
def pi.borel_space {ι : Type u_1} {π : ι → Type u_2} [fintype ι] [t' : Π (i : ι), topological_space («π» i)] [Π (i : ι), measurable_space («π» i)] [∀ (i : ι), ] [∀ (i : ι), borel_space («π» i)] :
borel_space (Π (i : ι), «π» i)
@[protected, instance]
def prod.borel_space {α : Type u_1} {β : Type u_2} [borel_space α] [borel_space β]  :
borel_space × β)
theorem closed_embedding.measurable_inv_fun {β : Type u_2} {γ : Type u_3} [borel_space β] [borel_space γ] [n : nonempty β] {g : β → γ} (hg : closed_embedding g) :
theorem measurable_comp_iff_of_closed_embedding {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [borel_space β] [borel_space γ] {f : δ → β} (g : β → γ) (hg : closed_embedding g) :
theorem ae_measurable_comp_iff_of_closed_embedding {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [borel_space β] [borel_space γ] {f : δ → β} {μ : measure_theory.measure δ} (g : β → γ) (hg : closed_embedding g) :
theorem ae_measurable_comp_right_iff_of_closed_embedding {α : Type u_1} {β : Type u_2} {δ : Type u_5} [borel_space α] [borel_space β] {g : α → β} {μ : measure_theory.measure α} {f : β → δ} (hg : closed_embedding g) :
ae_measurable (f g) μ μ)
theorem measurable_of_Iio {α : Type u_1} {δ : Type u_5} [borel_space α] [linear_order α] {f : δ → α} (hf : ∀ (x : α), measurable_set (f ⁻¹' set.Iio x)) :
theorem measurable_of_Ioi {α : Type u_1} {δ : Type u_5} [borel_space α] [linear_order α] {f : δ → α} (hf : ∀ (x : α), measurable_set (f ⁻¹' set.Ioi x)) :
theorem measurable_of_Iic {α : Type u_1} {δ : Type u_5} [borel_space α] [linear_order α] {f : δ → α} (hf : ∀ (x : α), measurable_set (f ⁻¹' set.Iic x)) :
theorem measurable_of_Ici {α : Type u_1} {δ : Type u_5} [borel_space α] [linear_order α] {f : δ → α} (hf : ∀ (x : α), measurable_set (f ⁻¹' set.Ici x)) :
theorem measurable.is_lub {α : Type u_1} {δ : Type u_5} [borel_space α] [linear_order α] {ι : Type u_2} [encodable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ (i : ι), measurable (f i)) (hg : ∀ (b : δ), is_lub {a : α | ∃ (i : ι), f i b = a} (g b)) :
theorem ae_measurable.is_lub {α : Type u_1} {δ : Type u_5} [borel_space α] [linear_order α] {ι : Type u_2} {μ : measure_theory.measure δ} [encodable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ (i : ι), ae_measurable (f i) μ) (hg : ∀ᵐ (b : δ) ∂μ, is_lub {a : α | ∃ (i : ι), f i b = a} (g b)) :
theorem measurable.is_glb {α : Type u_1} {δ : Type u_5} [borel_space α] [linear_order α] {ι : Type u_2} [encodable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ (i : ι), measurable (f i)) (hg : ∀ (b : δ), is_glb {a : α | ∃ (i : ι), f i b = a} (g b)) :
theorem ae_measurable.is_glb {α : Type u_1} {δ : Type u_5} [borel_space α] [linear_order α] {ι : Type u_2} {μ : measure_theory.measure δ} [encodable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ (i : ι), ae_measurable (f i) μ) (hg : ∀ᵐ (b : δ) ∂μ, is_glb {a : α | ∃ (i : ι), f i b = a} (g b)) :
theorem measurable.supr_Prop {δ : Type u_5} {α : Type u_1} (p : Prop) {f : δ → α} (hf : measurable f) :
measurable (λ (b : δ), ⨆ (h : p), f b)
theorem measurable.infi_Prop {δ : Type u_5} {α : Type u_1} (p : Prop) {f : δ → α} (hf : measurable f) :
measurable (λ (b : δ), ⨅ (h : p), f b)
theorem measurable_supr {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Type u_2} [encodable ι] {f : ι → δ → α} (hf : ∀ (i : ι), measurable (f i)) :
measurable (λ (b : δ), ⨆ (i : ι), f i b)
theorem ae_measurable_supr {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Type u_2} {μ : measure_theory.measure δ} [encodable ι] {f : ι → δ → α} (hf : ∀ (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (b : δ), ⨆ (i : ι), f i b) μ
theorem measurable_infi {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Type u_2} [encodable ι] {f : ι → δ → α} (hf : ∀ (i : ι), measurable (f i)) :
measurable (λ (b : δ), ⨅ (i : ι), f i b)
theorem ae_measurable_infi {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Type u_2} {μ : measure_theory.measure δ} [encodable ι] {f : ι → δ → α} (hf : ∀ (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (b : δ), ⨅ (i : ι), f i b) μ
theorem measurable_bsupr {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Type u_2} (s : set ι) {f : ι → δ → α} (hs : s.countable) (hf : ∀ (i : ι), measurable (f i)) :
measurable (λ (b : δ), ⨆ (i : ι) (H : i s), f i b)
theorem ae_measurable_bsupr {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Type u_2} {μ : measure_theory.measure δ} (s : set ι) {f : ι → δ → α} (hs : s.countable) (hf : ∀ (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (b : δ), ⨆ (i : ι) (H : i s), f i b) μ
theorem measurable_binfi {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Type u_2} (s : set ι) {f : ι → δ → α} (hs : s.countable) (hf : ∀ (i : ι), measurable (f i)) :
measurable (λ (b : δ), ⨅ (i : ι) (H : i s), f i b)
theorem ae_measurable_binfi {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Type u_2} {μ : measure_theory.measure δ} (s : set ι) {f : ι → δ → α} (hs : s.countable) (hf : ∀ (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (b : δ), ⨅ (i : ι) (H : i s), f i b) μ
theorem measurable_liminf' {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Type u_2} {ι' : Type u_3} {f : ι → δ → α} {u : filter ι} (hf : ∀ (i : ι), measurable (f i)) {p : ι' → Prop} {s : ι' → set ι} (hu : s) (hs : ∀ (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_5} [borel_space α] {ι : Type u_2} {ι' : Type u_3} {f : ι → δ → α} {u : filter ι} (hf : ∀ (i : ι), measurable (f i)) {p : ι' → Prop} {s : ι' → set ι} (hu : s) (hs : ∀ (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_5} [borel_space α] {f : δ → α} (hf : ∀ (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_5} [borel_space α] {f : δ → α} (hf : ∀ (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_5} [borel_space α] {ι : Type u_2} {f : ι → δ → α} {s : set ι} (hs : s.countable) (hf : ∀ (i : ι), measurable (f i)) (bdd : ∀ (x : δ), bdd_above ((λ (i : ι), f i x) '' s)) :
measurable (λ (x : δ), Sup ((λ (i : ι), f i x) '' s))
def homemorph.to_measurable_equiv {α : Type u_1} {β : Type u_2} [borel_space α] [borel_space β] (h : α ≃ₜ β) :
α ≃ᵐ β

Convert a homeomorph to a measurable_equiv.

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
theorem measurable_set_ball {α : Type u_1} [metric_space α] {x : α} {ε : } :
theorem measurable_set_closed_ball {α : Type u_1} [metric_space α] {x : α} {ε : } :
theorem measurable_inf_dist {α : Type u_1} [metric_space α] {s : set α} :
measurable (λ (x : α), s)
theorem measurable.inf_dist {α : Type u_1} {β : Type u_2} [metric_space α] {f : β → α} (hf : measurable f) {s : set α} :
measurable (λ (x : β), metric.inf_dist (f x) s)
theorem measurable_inf_nndist {α : Type u_1} [metric_space α] {s : set α} :
measurable (λ (x : α),
theorem measurable.inf_nndist {α : Type u_1} {β : Type u_2} [metric_space α] {f : β → α} (hf : measurable f) {s : set α} :
measurable (λ (x : β), metric.inf_nndist (f x) s)
theorem measurable_dist {α : Type u_1} [metric_space α]  :
measurable (λ (p : α × α), dist p.fst p.snd)
theorem measurable.dist {α : Type u_1} {β : Type u_2} [metric_space α] {f g : β → α} (hf : measurable f) (hg : measurable g) :
measurable (λ (b : β), dist (f b) (g b))
theorem measurable_nndist {α : Type u_1} [metric_space α]  :
measurable (λ (p : α × α), p.snd)
theorem measurable.nndist {α : Type u_1} {β : Type u_2} [metric_space α] {f g : β → α} (hf : measurable f) (hg : measurable g) :
measurable (λ (b : β), nndist (f b) (g b))
theorem measurable_set_eball {α : Type u_1} {x : α} {ε : ℝ≥0∞} :
theorem measurable_edist_right {α : Type u_1} {x : α} :
theorem measurable_edist_left {α : Type u_1} {x : α} :
measurable (λ (y : α), x)
theorem measurable_inf_edist {α : Type u_1} {s : set α} :
measurable (λ (x : α),
theorem measurable.inf_edist {α : Type u_1} {β : Type u_2} {f : β → α} (hf : measurable f) {s : set α} :
measurable (λ (x : β), emetric.inf_edist (f x) s)
theorem measurable_edist {α : Type u_1}  :
measurable (λ (p : α × α), edist p.fst p.snd)
theorem measurable.edist {α : Type u_1} {β : Type u_2} {f g : β → α} (hf : measurable f) (hg : measurable g) :
measurable (λ (b : β), edist (f b) (g b))
theorem ae_measurable.edist {α : Type u_1} {β : Type u_2} {f g : β → α} {μ : measure_theory.measure β} (hf : μ) (hg : μ) :
ae_measurable (λ (a : β), edist (f a) (g a)) μ
theorem real.measure_ext_Ioo_rat {μ ν : measure_theory.measure } (h : ∀ (a b : ), μ (set.Ioo a b) = ν (set.Ioo a b)) :
μ = ν
theorem measurable.nnreal_of_real {α : Type u_1} {f : α → } (hf : measurable f) :
measurable (λ (x : α), nnreal.of_real (f x))
theorem measurable.nnreal_coe {α : Type u_1} {f : α → ℝ≥0} (hf : measurable f) :
measurable (λ (x : α), (f x))
theorem measurable.ennreal_coe {α : Type u_1} {f : α → ℝ≥0} (hf : measurable f) :
measurable (λ (x : α), (f x))
theorem ae_measurable.ennreal_coe {α : Type u_1} {f : α → ℝ≥0} {μ : measure_theory.measure α} (hf : μ) :
ae_measurable (λ (x : α), (f x)) μ
theorem measurable.ennreal_of_real {α : Type u_1} {f : α → } (hf : measurable f) :
measurable (λ (x : α), ennreal.of_real (f x))

The set of finite ℝ≥0∞ numbers is measurable_equiv to ℝ≥0.

Equations
theorem ennreal.measurable_of_measurable_nnreal {α : Type u_1} {f : ℝ≥0∞ → α} (h : measurable (λ (p : ℝ≥0), f p)) :

ℝ≥0∞ is measurable_equiv to ℝ≥0 ⊕ unit.

Equations
theorem ennreal.measurable_of_measurable_nnreal_prod {β : Type u_2} {γ : Type u_3} {f : → γ} (H₁ : measurable (λ (p : ℝ≥0 × β), f ((p.fst), p.snd))) (H₂ : measurable (λ (x : β), f (, x))) :
theorem ennreal.measurable_of_measurable_nnreal_nnreal {β : Type u_2} {f : → β} (h₁ : measurable (λ (p : , f ((p.fst), (p.snd)))) (h₂ : measurable (λ (r : ℝ≥0), f (, r))) (h₃ : measurable (λ (r : ℝ≥0), f (r, ))) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem measurable.to_nnreal {α : Type u_1} {f : α → ℝ≥0∞} (hf : measurable f) :
measurable (λ (x : α), (f x).to_nnreal)
theorem measurable_ennreal_coe_iff {α : Type u_1} {f : α → ℝ≥0} :
measurable (λ (x : α), (f x))
theorem measurable.to_real {α : Type u_1} {f : α → ℝ≥0∞} (hf : measurable f) :
measurable (λ (x : α), (f x).to_real)
theorem ae_measurable.to_real {α : Type u_1} {f : α → ℝ≥0∞} {μ : measure_theory.measure α} (hf : μ) :
ae_measurable (λ (x : α), (f x).to_real) μ
theorem measurable.ennreal_tsum {α : Type u_1} {ι : Type u_2} [encodable ι] {f : ι → α → ℝ≥0∞} (h : ∀ (i : ι), measurable (f i)) :
measurable (λ (x : α), ∑' (i : ι), f i x)

note: ℝ≥0∞ can probably be generalized in a future version of this lemma.

theorem ae_measurable.ennreal_tsum {α : Type u_1} {ι : Type u_2} [encodable ι] {f : ι → α → ℝ≥0∞} {μ : measure_theory.measure α} (h : ∀ (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (x : α), ∑' (i : ι), f i x) μ
theorem measurable_norm {α : Type u_1} [normed_group α]  :
theorem measurable.norm {α : Type u_1} {β : Type u_2} [normed_group α] {f : β → α} (hf : measurable f) :
measurable (λ (a : β), f a)
theorem ae_measurable.norm {α : Type u_1} {β : Type u_2} [normed_group α] {f : β → α} {μ : measure_theory.measure β} (hf : μ) :
ae_measurable (λ (a : β), f a) μ
theorem measurable_nnnorm {α : Type u_1} [normed_group α]  :
theorem measurable.nnnorm {α : Type u_1} {β : Type u_2} [normed_group α] {f : β → α} (hf : measurable f) :
measurable (λ (a : β), nnnorm (f a))
theorem ae_measurable.nnnorm {α : Type u_1} {β : Type u_2} [normed_group α] {f : β → α} {μ : measure_theory.measure β} (hf : μ) :
ae_measurable (λ (a : β), nnnorm (f a)) μ
theorem measurable_ennnorm {α : Type u_1} [normed_group α]  :
measurable (λ (x : α), (nnnorm x))
theorem measurable.ennnorm {α : Type u_1} {β : Type u_2} [normed_group α] {f : β → α} (hf : measurable f) :
measurable (λ (a : β), (nnnorm (f a)))
theorem ae_measurable.ennnorm {α : Type u_1} {β : Type u_2} [normed_group α] {f : β → α} {μ : measure_theory.measure β} (hf : μ) :
ae_measurable (λ (a : β), (nnnorm (f a))) μ
theorem measurable_of_tendsto_nnreal' {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} {f : ι → α → ℝ≥0} {g : α → ℝ≥0} (u : filter ι) [u.ne_bot] (hf : ∀ (i : ι), measurable (f i)) (lim : (𝓝 g)) {p : ι' → Prop} {s : ι' → set ι} (hu : s) (hs : ∀ (i : ι'), (s i).countable) :

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} {f : α → ℝ≥0} {g : α → ℝ≥0} (hf : ∀ (i : ), measurable (f i)) (lim : (𝓝 g)) :

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

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

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} [metric_space β] [borel_space β] {f : α → β} {g : α → β} (hf : ∀ (i : ), measurable (f i)) (lim : (𝓝 g)) :

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

theorem ae_measurable_of_tendsto_metric_ae {α : Type u_1} {β : Type u_2} [metric_space β] [borel_space β] {μ : measure_theory.measure α} {f : α → β} {g : α → β} (hf : ∀ (n : ), ae_measurable (f n) μ) (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ), f n x) filter.at_top (𝓝 (g x))) :
theorem measurable_of_tendsto_metric_ae {α : Type u_1} {β : Type u_2} [metric_space β] [borel_space β] {μ : measure_theory.measure α} [μ.is_complete] {f : α → β} {g : α → β} (hf : ∀ (n : ), measurable (f n)) (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ), f n x) filter.at_top (𝓝 (g x))) :
theorem measurable_limit_of_tendsto_metric_ae {α : Type u_1} {β : Type u_2} [metric_space β] [borel_space β] {μ : measure_theory.measure α} {f : α → β} (hf : ∀ (n : ), ae_measurable (f n) μ) (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), filter.tendsto (λ (n : ), f n x) filter.at_top (𝓝 l)) :
∃ (f_lim : α → β) (hf_lim_meas : measurable f_lim), ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ), f n x) filter.at_top (𝓝 (f_lim x))
@[protected]
theorem continuous_linear_map.measurable {𝕜 : Type u_6} [normed_field 𝕜] {E : Type u_7} [normed_group E] [ E] {F : Type u_8} [normed_group F] [ F] [borel_space F] (L : E →L[𝕜] F) :
theorem continuous_linear_map.measurable_comp {α : Type u_1} {𝕜 : Type u_6} [normed_field 𝕜] {E : Type u_7} [normed_group E] [ E] {F : Type u_8} [normed_group F] [ F] [borel_space F] (L : E →L[𝕜] F) {φ : α → E} (φ_meas : measurable φ) :
measurable (λ (a : α), L (φ a))
@[protected, instance]
def continuous_linear_map.measurable_space {𝕜 : Type u_6} {E : Type u_7} [normed_group E] [ E] {F : Type u_8} [normed_group F] [ F] :
Equations
@[protected, instance]
def continuous_linear_map.borel_space {𝕜 : Type u_6} {E : Type u_7} [normed_group E] [ E] {F : Type u_8} [normed_group F] [ F] :
theorem continuous_linear_map.measurable_apply {𝕜 : Type u_6} {E : Type u_7} [normed_group E] [ E] {F : Type u_8} [normed_group F] [ F] [borel_space F] (x : E) :
measurable (λ (f : E →L[𝕜] F), f x)
theorem continuous_linear_map.measurable_apply' {𝕜 : Type u_6} {E : Type u_7} [normed_group E] [ E] {F : Type u_8} [normed_group F] [ F] [borel_space F] :
measurable (λ (x : E) (f : E →L[𝕜] F), f x)
theorem continuous_linear_map.measurable_coe {𝕜 : Type u_6} {E : Type u_7} [normed_group E] [ E] {F : Type u_8} [normed_group F] [ F] [borel_space F] :
measurable (λ (f : E →L[𝕜] F) (x : E), f x)
theorem measurable.apply_continuous_linear_map {α : Type u_1} {𝕜 : Type u_6} {E : Type u_7} [normed_group E] [ E] [borel_space E] {F : Type u_8} [normed_group F] [ F] {φ : α → (F →L[𝕜] E)} (hφ : measurable φ) (v : F) :
measurable (λ (a : α), (φ a) v)
theorem ae_measurable.apply_continuous_linear_map {α : Type u_1} {𝕜 : Type u_6} {E : Type u_7} [normed_group E] [ E] [borel_space E] {F : Type u_8} [normed_group F] [ F] {φ : α → (F →L[𝕜] E)} {μ : measure_theory.measure α} (hφ : μ) (v : F) :
ae_measurable (λ (a : α), (φ a) v) μ
theorem measurable_smul_const {α : Type u_1} {𝕜 : Type u_6} [borel_space 𝕜] {E : Type u_7} [normed_group E] [ E] [borel_space E] {f : α → 𝕜} {c : E} (hc : c 0) :
measurable (λ (x : α), f x c)
theorem ae_measurable_smul_const {α : Type u_1} {𝕜 : Type u_6} [borel_space 𝕜] {E : Type u_7} [normed_group E] [ E] [borel_space E] {f : α → 𝕜} {μ : measure_theory.measure α} {c : E} (hc : c 0) :
ae_measurable (λ (x : α), f x c) μ
structure measure_theory.measure.regular {α : Type u_1} (μ : measure_theory.measure α) :
Prop
• lt_top_of_is_compact : ∀ ⦃K : set α⦄, μ K <
• outer_regular : ∀ ⦃A : set α⦄, (⨅ (U : set α) (h : is_open U) (h2 : A U), μ U) μ A
• inner_regular : ∀ ⦃U : set α⦄, (μ U ⨆ (K : set α) (h : (h2 : K U), μ K)

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} {μ : measure_theory.measure α} (hμ : μ.regular) ⦃A : set α⦄ (hA : measurable_set A) :
(⨅ (U : set α) (h : is_open U) (h2 : A U), μ U) = μ A
theorem measure_theory.measure.regular.inner_regular_eq {α : Type u_1} {μ : measure_theory.measure α} (hμ : μ.regular) ⦃U : set α⦄ (hU : is_open U) :
(⨆ (K : set α) (h : (h2 : K U), μ K) = μ U
theorem measure_theory.measure.regular.exists_compact_not_null {α : Type u_1} {μ : measure_theory.measure α} (hμ : μ.regular) :
(∃ (K : set α), μ K 0) μ 0
@[protected]
theorem measure_theory.measure.regular.map {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [t2_space β] [borel_space β] (hμ : μ.regular) (f : α ≃ₜ β) :
μ).regular
@[protected]
theorem measure_theory.measure.regular.smul {α : Type u_1} {μ : measure_theory.measure α} (hμ : μ.regular) {x : ℝ≥0∞} (hx : x < ) :
(x μ).regular
@[protected]
theorem measure_theory.measure.regular.sigma_finite {α : Type u_1} {μ : measure_theory.measure α} [t2_space α] (hμ : μ.regular) :

A regular measure in a σ-compact space is σ-finite.

theorem is_compact.measure_lt_top_of_nhds_within {α : Type u_1} {s : set α} {μ : measure_theory.measure α} (h : is_compact s) (hμ : ∀ (x : α), x sμ.finite_at_filter (𝓝[s] x)) :
μ s <
theorem is_compact.measure_lt_top {α : Type u_1} {s : set α} {μ : measure_theory.measure α} (h : is_compact s) :
μ s <