mathlib3 documentation

measure_theory.constructions.borel_space.basic

Borel (measurable) space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

Main statements #

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

measurable_space structure generated by topological_space.

Equations
theorem borel_anti {α : Type u_1} :
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 : α β} (hf : continuous f) :
@[class]
structure opens_measurable_space (α : Type u_6) [topological_space α] [h : measurable_space α] :
Prop

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

Instances of this typeclass

Add instances borel α : measurable_space α and ⟨rfl⟩ : borel_space α.

meta def tactic.borel_to_refl (α i : expr) :

Given a type α, an assumption i : measurable_space α, and an instance [borel_space α], replace i with borel α.

meta def tactic.borelize (α : expr) :

Given a type α, if there is an assumption [i : measurable_space α], then try to prove [borel_space α] and replace i with borel α. Otherwise, add instances borel α : measurable_space α and ⟨rfl⟩ : borel_space α.

The behaviour of borelize α depends on the existing assumptions on α.

Finally, borelize [α, β, γ] runs borelize α, borelize β, borelize γ.

The behaviour of borelize α depends on the existing assumptions on α.

Finally, borelize [α, β, γ] runs borelize α, borelize β, borelize γ.

@[protected, instance]
@[protected, instance]

In a borel_space all open sets are measurable.

@[protected, instance]
def subtype.borel_space {α : Type u_1} [topological_space α] [measurable_space α] [hα : borel_space α] (s : set α) :
theorem measurable_set.induction_on_open {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] {C : set α Prop} (h_open : (U : set α), is_open U C U) (h_compl : (t : set α), measurable_set t C t C t) (h_union : (f : set α), pairwise (disjoint on f) ( (i : ), measurable_set (f i)) ( (i : ), C (f i)) C ( (i : ), f i)) ⦃t : set α⦄ :
@[measurability]
@[measurability]
theorem measurable_of_is_open {γ : Type u_3} {δ : Type u_5} [topological_space γ] [measurable_space γ] [borel_space γ] [measurable_space δ] {f : δ γ} (hf : (s : set γ), is_open s measurable_set (f ⁻¹' s)) :
theorem measurable_of_is_closed {γ : Type u_3} {δ : Type u_5} [topological_space γ] [measurable_space γ] [borel_space γ] [measurable_space δ] {f : δ γ} (hf : (s : set γ), is_closed s measurable_set (f ⁻¹' s)) :
theorem measurable_of_is_closed' {γ : Type u_3} {δ : Type u_5} [topological_space γ] [measurable_space γ] [borel_space γ] [measurable_space δ] {f : δ γ} (hf : (s : set γ), is_closed s s.nonempty s set.univ measurable_set (f ⁻¹' s)) :

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]
def pi.opens_measurable_space {ι : Type u_1} {π : ι Type u_2} [countable ι] [t' : Π (i : ι), topological_space (π i)] [Π (i : ι), measurable_space (π i)] [ (i : ι), topological_space.second_countable_topology (π i)] [ (i : ι), opens_measurable_space (π i)] :
opens_measurable_space (Π (i : ι), π i)
theorem interior_ae_eq_of_null_frontier {α' : Type u_6} [topological_space α'] [measurable_space α'] {μ : measure_theory.measure α'} {s : set α'} (h : μ (frontier s) = 0) :
theorem measure_interior_of_null_frontier {α' : Type u_6} [topological_space α'] [measurable_space α'] {μ : measure_theory.measure α'} {s : set α'} (h : μ (frontier s) = 0) :
μ (interior s) = μ s
theorem closure_ae_eq_of_null_frontier {α' : Type u_6} [topological_space α'] [measurable_space α'] {μ : measure_theory.measure α'} {s : set α'} (h : μ (frontier s) = 0) :
theorem measure_closure_of_null_frontier {α' : Type u_6} [topological_space α'] [measurable_space α'] {μ : measure_theory.measure α'} {s : set α'} (h : μ (frontier s) = 0) :
μ (closure s) = μ s
@[simp, measurability]
@[simp, measurability]
@[simp, measurability]
@[measurability]
@[simp, measurability]
@[simp, measurability]
@[simp, measurability]
@[simp, measurability]
@[simp, measurability]
@[measurability]
theorem generate_from_Ico_mem_le_borel {α : Type u_1} [topological_space α] [linear_order α] [order_closed_topology α] (s t : set α) :
measurable_space.generate_from {S : set α | (l : α) (H : l s) (u : α) (H : u t) (h : l < u), set.Ico l u = S} borel α
theorem dense.borel_eq_generate_from_Ico_mem_aux {α : Type u_1} [topological_space α] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] {s : set α} (hd : dense s) (hbot : (x : α), is_bot x x s) (hIoo : (x y : α), x < y set.Ioo x y = y s) :
borel α = measurable_space.generate_from {S : set α | (l : α) (H : l s) (u : α) (H : u s) (h : l < u), set.Ico l u = S}
theorem dense.borel_eq_generate_from_Ico_mem {α : Type u_1} [topological_space α] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] [densely_ordered α] [no_min_order α] {s : set α} (hd : dense s) :
borel α = measurable_space.generate_from {S : set α | (l : α) (H : l s) (u : α) (H : u s) (h : l < u), set.Ico l u = S}
theorem dense.borel_eq_generate_from_Ioc_mem_aux {α : Type u_1} [topological_space α] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] {s : set α} (hd : dense s) (hbot : (x : α), is_top x x s) (hIoo : (x y : α), x < y set.Ioo x y = x s) :
borel α = measurable_space.generate_from {S : set α | (l : α) (H : l s) (u : α) (H : u s) (h : l < u), set.Ioc l u = S}
theorem dense.borel_eq_generate_from_Ioc_mem {α : Type u_1} [topological_space α] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] [densely_ordered α] [no_max_order α] {s : set α} (hd : dense s) :
borel α = measurable_space.generate_from {S : set α | (l : α) (H : l s) (u : α) (H : u s) (h : l < u), set.Ioc l u = S}

Two finite measures on a Borel space are equal if they agree on all closed-open intervals. If α is a conditionally complete linear order with no top element, measure_theory.measure..ext_of_Ico is an extensionality lemma with weaker assumptions on μ and ν.

Two finite measures on a Borel space are equal if they agree on all open-closed intervals. If α is a conditionally complete linear order with no top element, measure_theory.measure..ext_of_Ioc is an extensionality lemma with weaker assumptions on μ and ν.

theorem measure_theory.measure.ext_of_Ico' {α : Type u_1} [topological_space α] {m : measurable_space α} [topological_space.second_countable_topology α] [linear_order α] [order_topology α] [borel_space α] [no_max_order α] (μ ν : measure_theory.measure α) (hμ : ⦃a b : α⦄, a < b μ (set.Ico a b) ) (h : ⦃a b : α⦄, a < b μ (set.Ico a b) = ν (set.Ico a b)) :
μ = ν

Two measures which are finite on closed-open intervals are equal if the agree on all closed-open intervals.

theorem measure_theory.measure.ext_of_Ioc' {α : Type u_1} [topological_space α] {m : measurable_space α} [topological_space.second_countable_topology α] [linear_order α] [order_topology α] [borel_space α] [no_min_order α] (μ ν : measure_theory.measure α) (hμ : ⦃a b : α⦄, a < b μ (set.Ioc a b) ) (h : ⦃a b : α⦄, a < b μ (set.Ioc a b) = ν (set.Ioc a b)) :
μ = ν

Two measures which are finite on closed-open intervals are equal if the agree on all open-closed intervals.

Two measures which are finite on closed-open intervals are equal if the agree on all closed-open intervals.

Two measures which are finite on closed-open intervals are equal if the agree on all open-closed intervals.

Two finite measures on a Borel space are equal if they agree on all left-infinite right-closed intervals.

Two finite measures on a Borel space are equal if they agree on all left-closed right-infinite intervals.

@[measurability]
@[measurability]
@[measurability]
@[measurability]

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

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

theorem continuous_on.measurable_piecewise {α : Type u_1} {γ : Type u_3} [topological_space α] [measurable_space α] [opens_measurable_space α] [topological_space γ] [measurable_space γ] [borel_space γ] {f g : α γ} {s : set α} [Π (j : α), decidable (j s)] (hf : continuous_on f s) (hg : continuous_on g s) (hs : measurable_set s) :

If a function is defined piecewise in terms of functions which are continuous on their respective pieces, then it is measurable.

@[protected, measurability]
def homeomorph.to_measurable_equiv {γ : Type u_3} {γ₂ : Type u_4} [topological_space γ] [measurable_space γ] [borel_space γ] [topological_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} [topological_space γ] [measurable_space γ] [borel_space γ] [topological_space γ₂] [measurable_space γ₂] [borel_space γ₂] (h : γ ≃ₜ γ₂) :
@[simp]
@[measurability]
theorem continuous.measurable2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [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 : α β γ} (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} [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 : α β γ} {μ : measure_theory.measure δ} (h : continuous (λ (p : α × β), c p.fst p.snd)) (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (a : δ), c (f a) (g a)) μ
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)
@[protected, instance]
def pi.borel_space {ι : Type u_1} {π : ι Type u_2} [countable ι] [Π (i : ι), topological_space (π i)] [Π (i : ι), measurable_space (π i)] [ (i : ι), topological_space.second_countable_topology (π i)] [ (i : ι), borel_space (π i)] :
borel_space (Π (i : ι), π i)
@[protected]
theorem measurable.is_lub {α : Type u_1} {δ : Type u_5} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Sort u_2} [countable ι] {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} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Sort u_2} {μ : measure_theory.measure δ} [countable ι] {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} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Sort u_2} [countable ι] {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} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Sort u_2} {μ : measure_theory.measure δ} [countable ι] {f : ι δ α} {g : δ α} (hf : (i : ι), ae_measurable (f i) μ) (hg : ∀ᵐ (b : δ) μ, is_glb {a : α | (i : ι), f i b = a} (g b)) :
theorem measurable_set_of_mem_nhds_within_Ioi_aux {α : Type u_1} [topological_space α] [measurable_space α] [borel_space α] [linear_order α] [order_topology α] [topological_space.second_countable_topology α] {s : set α} (h : (x : α), x s s nhds_within x (set.Ioi x)) (h' : (x : α), x s ( (y : α), x < y)) :

If a set is a right-neighborhood of all of its points, then it is measurable.

@[measurability]
theorem measurable.supr_Prop {δ : Type u_5} [measurable_space δ] {α : Type u_1} [measurable_space α] [complete_lattice α] (p : Prop) {f : δ α} (hf : measurable f) :
measurable (λ (b : δ), (h : p), f b)
@[measurability]
theorem measurable.infi_Prop {δ : Type u_5} [measurable_space δ] {α : Type u_1} [measurable_space α] [complete_lattice α] (p : Prop) {f : δ α} (hf : measurable f) :
measurable (λ (b : δ), (h : p), f b)
@[measurability]
theorem measurable_supr {α : Type u_1} {δ : Type u_5} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Sort u_2} [countable ι] {f : ι δ α} (hf : (i : ι), measurable (f i)) :
measurable (λ (b : δ), (i : ι), f i b)
@[measurability]
theorem ae_measurable_supr {α : Type u_1} {δ : Type u_5} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Sort u_2} {μ : measure_theory.measure δ} [countable ι] {f : ι δ α} (hf : (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (b : δ), (i : ι), f i b) μ
@[measurability]
theorem measurable_infi {α : Type u_1} {δ : Type u_5} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Sort u_2} [countable ι] {f : ι δ α} (hf : (i : ι), measurable (f i)) :
measurable (λ (b : δ), (i : ι), f i b)
@[measurability]
theorem ae_measurable_infi {α : Type u_1} {δ : Type u_5} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Sort u_2} {μ : measure_theory.measure δ} [countable ι] {f : ι δ α} (hf : (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (b : δ), (i : ι), f i b) μ
theorem measurable_bsupr {α : Type u_1} {δ : Type u_5} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : 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} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : 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} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : 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} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : 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} [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 ι} (hu : u.has_countable_basis p s) (hs : (i : ι'), (s i).countable) :
measurable (λ (x : δ), filter.liminf (λ (i : ι), f i x) u)

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

theorem measurable_limsup' {α : Type u_1} {δ : Type u_5} [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 ι} (hu : u.has_countable_basis p s) (hs : (i : ι'), (s i).countable) :
measurable (λ (x : δ), filter.limsup (λ (i : ι), f i x) u)

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

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

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

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

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

theorem measurable_cSup {α : Type u_1} {δ : Type u_5} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [conditionally_complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : 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 : δ), has_Sup.Sup ((λ (i : ι), f i x) '' s))
theorem measurable_cInf {α : Type u_1} {δ : Type u_5} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [conditionally_complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Type u_2} {f : ι δ α} {s : set ι} (hs : s.countable) (hf : (i : ι), measurable (f i)) (bdd : (x : δ), bdd_below ((λ (i : ι), f i x) '' s)) :
measurable (λ (x : δ), has_Inf.Inf ((λ (i : ι), f i x) '' s))
theorem measurable_csupr {α : Type u_1} {δ : Type u_5} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [conditionally_complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Type u_2} [countable ι] {f : ι δ α} (hf : (i : ι), measurable (f i)) (bdd : (x : δ), bdd_above (set.range (λ (i : ι), f i x))) :
measurable (λ (x : δ), (i : ι), f i x)
theorem measurable_cinfi {α : Type u_1} {δ : Type u_5} [topological_space α] [measurable_space α] [borel_space α] [measurable_space δ] [conditionally_complete_linear_order α] [order_topology α] [topological_space.second_countable_topology α] {ι : Type u_2} [countable ι] {f : ι δ α} (hf : (i : ι), measurable (f i)) (bdd : (x : δ), bdd_below (set.range (λ (i : ι), f i x))) :
measurable (λ (x : δ), (i : ι), f i x)
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow {α : Type u_1} [measurable_space α] (μ : measure_theory.measure α) {f : α ennreal} (hf : measurable f) {s : set α} (hs : measurable_set s) {t : nnreal} (ht : 1 < t) :
μ s = μ (s f ⁻¹' {0}) + μ (s f ⁻¹' {}) + ∑' (n : ), μ (s f ⁻¹' set.Ico (t ^ n) (t ^ (n + 1)))

One can cut out ℝ≥0∞ into the sets {0}, Ico (t^n) (t^(n+1)) for n : ℤ and {∞}. This gives a way to compute the measure of a set in terms of sets on which a given function f does not fluctuate by more than t.

@[measurability]
@[measurability]
@[measurability]
theorem measurable_inf_dist {α : Type u_1} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] {s : set α} :
measurable (λ (x : α), metric.inf_dist x s)
@[measurability]
theorem measurable.inf_dist {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] {f : β α} (hf : measurable f) {s : set α} :
measurable (λ (x : β), metric.inf_dist (f x) s)
@[measurability]
@[measurability]
theorem measurable.inf_nndist {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] {f : β α} (hf : measurable f) {s : set α} :
measurable (λ (x : β), metric.inf_nndist (f x) s)
@[measurability]
theorem measurable.dist {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] [topological_space.second_countable_topology α] {f g : β α} (hf : measurable f) (hg : measurable g) :
measurable (λ (b : β), has_dist.dist (f b) (g b))
@[measurability]
theorem measurable.nndist {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] [topological_space.second_countable_topology α] {f g : β α} (hf : measurable f) (hg : measurable g) :
measurable (λ (b : β), has_nndist.nndist (f b) (g b))
theorem tendsto_measure_cthickening {α : Type u_1} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] {μ : measure_theory.measure α} {s : set α} (hs : (R : ) (H : R > 0), μ (metric.cthickening R s) ) :
filter.tendsto (λ (r : ), μ (metric.cthickening r s)) (nhds 0) (nhds (μ (closure s)))

If a set has a closed thickening with finite measure, then the measure of its r-closed thickenings converges to the measure of its closure as r tends to 0.

theorem tendsto_measure_cthickening_of_is_closed {α : Type u_1} [pseudo_metric_space α] [measurable_space α] [opens_measurable_space α] {μ : measure_theory.measure α} {s : set α} (hs : (R : ) (H : R > 0), μ (metric.cthickening R s) ) (h's : is_closed s) :
filter.tendsto (λ (r : ), μ (metric.cthickening r s)) (nhds 0) (nhds (μ s))

If a closed set has a closed thickening with finite measure, then the measure of its r-closed thickenings converges to its measure as r tends to 0.

Given a compact set in a proper space, the measure of its r-closed thickenings converges to its measure as r tends to 0.

@[measurability]
@[measurability]
theorem measurable_edist_left {α : Type u_1} [pseudo_emetric_space α] [measurable_space α] [opens_measurable_space α] {x : α} :
measurable (λ (y : α), has_edist.edist y x)
@[measurability]
@[measurability]
theorem measurable.inf_edist {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] {f : β α} (hf : measurable f) {s : set α} :
measurable (λ (x : β), emetric.inf_edist (f x) s)
@[measurability]
theorem measurable.edist {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] [topological_space.second_countable_topology α] {f g : β α} (hf : measurable f) (hg : measurable g) :
measurable (λ (b : β), has_edist.edist (f b) (g b))
@[measurability]
theorem ae_measurable.edist {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [measurable_space α] [opens_measurable_space α] [measurable_space β] [topological_space.second_countable_topology α] {f g : β α} {μ : measure_theory.measure β} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
ae_measurable (λ (a : β), has_edist.edist (f a) (g a)) μ
theorem real.is_pi_system_Ioo_rat  :
is_pi_system ( (a b : ) (h : a < b), {set.Ioo a b})

The intervals (-(n + 1), (n + 1)) form a finite spanning sets in the set of open intervals with rational endpoints for a locally finite measure μ on .

Equations
@[measurability]
theorem measurable.real_to_nnreal {α : Type u_1} [measurable_space α] {f : α } (hf : measurable f) :
measurable (λ (x : α), (f x).to_nnreal)
@[measurability]
theorem ae_measurable.real_to_nnreal {α : Type u_1} [measurable_space α] {f : α } {μ : measure_theory.measure α} (hf : ae_measurable f μ) :
ae_measurable (λ (x : α), (f x).to_nnreal) μ
@[measurability]
@[measurability]
theorem measurable.coe_nnreal_real {α : Type u_1} [measurable_space α] {f : α nnreal} (hf : measurable f) :
measurable (λ (x : α), (f x))
@[measurability]
theorem ae_measurable.coe_nnreal_real {α : Type u_1} [measurable_space α] {f : α nnreal} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :
ae_measurable (λ (x : α), (f x)) μ
@[measurability]
@[measurability]
theorem measurable.coe_nnreal_ennreal {α : Type u_1} [measurable_space α] {f : α nnreal} (hf : measurable f) :
measurable (λ (x : α), (f x))
@[measurability]
theorem ae_measurable.coe_nnreal_ennreal {α : Type u_1} [measurable_space α] {f : α nnreal} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :
ae_measurable (λ (x : α), (f x)) μ
@[measurability]
theorem measurable.ennreal_of_real {α : Type u_1} [measurable_space α] {f : α } (hf : measurable f) :
measurable (λ (x : α), ennreal.of_real (f x))
@[simp, norm_cast]
theorem measurable_coe_nnreal_real_iff {α : Type u_1} [measurable_space α] {f : α nnreal} :
measurable (λ (x : α), (f x)) measurable f
@[simp, norm_cast]
theorem ae_measurable_coe_nnreal_real_iff {α : Type u_1} [measurable_space α] {f : α nnreal} {μ : measure_theory.measure α} :
ae_measurable (λ (x : α), (f x)) μ ae_measurable f μ
theorem ennreal.measurable_of_measurable_nnreal {α : Type u_1} [measurable_space α] {f : ennreal α} (h : measurable (λ (p : nnreal), f p)) :

ℝ≥0∞ 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 × β γ} (H₁ : measurable (λ (p : nnreal × β), f ((p.fst), p.snd))) (H₂ : measurable (λ (x : β), f (, x))) :
theorem ennreal.measurable_of_measurable_nnreal_nnreal {β : Type u_2} [measurable_space β] {f : ennreal × ennreal β} (h₁ : measurable (λ (p : nnreal × nnreal), f ((p.fst), (p.snd)))) (h₂ : measurable (λ (r : nnreal), f (, r))) (h₃ : measurable (λ (r : nnreal), f (r, ))) :
@[measurability]
theorem measurable.ennreal_to_nnreal {α : Type u_1} [measurable_space α] {f : α ennreal} (hf : measurable f) :
measurable (λ (x : α), (f x).to_nnreal)
@[measurability]
theorem ae_measurable.ennreal_to_nnreal {α : Type u_1} [measurable_space α] {f : α ennreal} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :
ae_measurable (λ (x : α), (f x).to_nnreal) μ
@[simp, norm_cast]
theorem measurable_coe_nnreal_ennreal_iff {α : Type u_1} [measurable_space α] {f : α nnreal} :
measurable (λ (x : α), (f x)) measurable f
@[simp, norm_cast]
theorem ae_measurable_coe_nnreal_ennreal_iff {α : Type u_1} [measurable_space α] {f : α nnreal} {μ : measure_theory.measure α} :
ae_measurable (λ (x : α), (f x)) μ ae_measurable f μ
@[measurability]
theorem measurable.ennreal_to_real {α : Type u_1} [measurable_space α] {f : α ennreal} (hf : measurable f) :
measurable (λ (x : α), (f x).to_real)
@[measurability]
theorem ae_measurable.ennreal_to_real {α : Type u_1} [measurable_space α] {f : α ennreal} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :
ae_measurable (λ (x : α), (f x).to_real) μ
@[measurability]
theorem measurable.ennreal_tsum {α : Type u_1} [measurable_space α] {ι : Type u_2} [countable ι] {f : ι α ennreal} (h : (i : ι), measurable (f i)) :
measurable (λ (x : α), ∑' (i : ι), f i x)

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

@[measurability]
theorem measurable.ennreal_tsum' {α : Type u_1} [measurable_space α] {ι : Type u_2} [countable ι] {f : ι α ennreal} (h : (i : ι), measurable (f i)) :
measurable (∑' (i : ι), f i)
@[measurability]
theorem measurable.nnreal_tsum {α : Type u_1} [measurable_space α] {ι : Type u_2} [countable ι] {f : ι α nnreal} (h : (i : ι), measurable (f i)) :
measurable (λ (x : α), ∑' (i : ι), f i x)
@[measurability]
theorem ae_measurable.ennreal_tsum {α : Type u_1} [measurable_space α] {ι : Type u_2} [countable ι] {f : ι α ennreal} {μ : measure_theory.measure α} (h : (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (x : α), ∑' (i : ι), f i x) μ
@[measurability]
theorem ae_measurable.nnreal_tsum {α : Type u_1} [measurable_space α] {ι : Type u_2} [countable ι] {f : ι α nnreal} {μ : measure_theory.measure α} (h : (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (x : α), ∑' (i : ι), f i x) μ
@[measurability]
@[measurability]
theorem measurable.coe_real_ereal {α : Type u_1} [measurable_space α] {f : α } (hf : measurable f) :
measurable (λ (x : α), (f x))
@[measurability]
theorem ae_measurable.coe_real_ereal {α : Type u_1} [measurable_space α] {f : α } {μ : measure_theory.measure α} (hf : ae_measurable f μ) :
ae_measurable (λ (x : α), (f x)) μ
theorem ereal.measurable_of_measurable_real {α : Type u_1} [measurable_space α] {f : ereal α} (h : measurable (λ (p : ), f p)) :
@[measurability]
theorem measurable.ereal_to_real {α : Type u_1} [measurable_space α] {f : α ereal} (hf : measurable f) :
measurable (λ (x : α), (f x).to_real)
@[measurability]
theorem ae_measurable.ereal_to_real {α : Type u_1} [measurable_space α] {f : α ereal} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :
ae_measurable (λ (x : α), (f x).to_real) μ
@[measurability]
@[measurability]
theorem measurable.coe_ereal_ennreal {α : Type u_1} [measurable_space α] {f : α ennreal} (hf : measurable f) :
measurable (λ (x : α), (f x))
@[measurability]
theorem ae_measurable.coe_ereal_ennreal {α : Type u_1} [measurable_space α] {f : α ennreal} {μ : measure_theory.measure α} (hf : ae_measurable f μ) :
ae_measurable (λ (x : α), (f x)) μ
@[measurability]
theorem measurable.norm {α : Type u_1} {β : Type u_2} [measurable_space α] [normed_add_comm_group α] [opens_measurable_space α] [measurable_space β] {f : β α} (hf : measurable f) :
measurable (λ (a : β), f a)
@[measurability]
theorem ae_measurable.norm {α : Type u_1} {β : Type u_2} [measurable_space α] [normed_add_comm_group α] [opens_measurable_space α] [measurable_space β] {f : β α} {μ : measure_theory.measure β} (hf : ae_measurable f μ) :
ae_measurable (λ (a : β), f a) μ
@[measurability]
theorem measurable.nnnorm {α : Type u_1} {β : Type u_2} [measurable_space α] [normed_add_comm_group α] [opens_measurable_space α] [measurable_space β] {f : β α} (hf : measurable f) :
measurable (λ (a : β), f a‖₊)
@[measurability]
theorem ae_measurable.nnnorm {α : Type u_1} {β : Type u_2} [measurable_space α] [normed_add_comm_group α] [opens_measurable_space α] [measurable_space β] {f : β α} {μ : measure_theory.measure β} (hf : ae_measurable f μ) :
ae_measurable (λ (a : β), f a‖₊) μ
@[measurability]
@[measurability]
theorem measurable.ennnorm {α : Type u_1} {β : Type u_2} [measurable_space α] [normed_add_comm_group α] [opens_measurable_space α] [measurable_space β] {f : β α} (hf : measurable f) :
measurable (λ (a : β), f a‖₊)
@[measurability]
theorem ae_measurable.ennnorm {α : Type u_1} {β : Type u_2} [measurable_space α] [normed_add_comm_group α] [opens_measurable_space α] [measurable_space β] {f : β α} {μ : measure_theory.measure β} (hf : ae_measurable f μ) :
ae_measurable (λ (a : β), f a‖₊) μ