# Borel sigma algebras on (pseudo-)metric spaces #

## Main statements #

• measurable_dist, measurable_infEdist, measurable_norm, Measurable.dist, Measurable.infEdist, Measurable.norm: measurability of various metric-related notions;
• tendsto_measure_thickening_of_isClosed: the measure of a closed set is the limit of the measure of its ε-thickenings as ε → 0.
• exists_borelSpace_of_countablyGenerated_of_separatesPoints: if a measurable space is countably generated and separates points, it arises as the Borel sets of some second countable separable metrizable topology.
theorem measurableSet_ball {α : Type u_1} [] {x : α} {ε : } :
theorem measurableSet_closedBall {α : Type u_1} [] {x : α} {ε : } :
theorem measurable_infDist {α : Type u_1} [] {s : Set α} :
Measurable fun (x : α) =>
theorem Measurable.infDist {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) {s : Set α} :
Measurable fun (x : β) => Metric.infDist (f x) s
theorem measurable_infNndist {α : Type u_1} [] {s : Set α} :
Measurable fun (x : α) =>
theorem Measurable.infNndist {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) {s : Set α} :
Measurable fun (x : β) => Metric.infNndist (f x) s
theorem measurable_dist {α : Type u_1} [] :
Measurable fun (p : α × α) => dist p.1 p.2
theorem Measurable.dist {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} (hf : ) (hg : ) :
Measurable fun (b : β) => dist (f b) (g b)
theorem measurable_nndist {α : Type u_1} [] :
Measurable fun (p : α × α) => nndist p.1 p.2
theorem Measurable.nndist {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} (hf : ) (hg : ) :
Measurable fun (b : β) => nndist (f b) (g b)
theorem measurableSet_eball {α : Type u_1} [] {x : α} {ε : ENNReal} :
theorem measurable_edist_right {α : Type u_1} [] {x : α} :
theorem measurable_edist_left {α : Type u_1} [] {x : α} :
Measurable fun (y : α) => edist y x
theorem measurable_infEdist {α : Type u_1} [] {s : Set α} :
Measurable fun (x : α) =>
theorem Measurable.infEdist {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) {s : Set α} :
Measurable fun (x : β) => EMetric.infEdist (f x) s
theorem tendsto_measure_cthickening {α : Type u_1} [] {μ : } {s : Set α} (hs : R > 0, μ () ) :
Filter.Tendsto (fun (r : ) => μ ()) (nhds 0) (nhds (μ ()))

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_isClosed {α : Type u_1} [] {μ : } {s : Set α} (hs : R > 0, μ () ) (h's : ) :
Filter.Tendsto (fun (r : ) => μ ()) (nhds 0) (nhds (μ s))

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

theorem tendsto_measure_thickening {α : Type u_1} [] {μ : } {s : Set α} (hs : R > 0, μ () ) :
Filter.Tendsto (fun (r : ) => μ ()) (nhdsWithin 0 ()) (nhds (μ ()))

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

theorem tendsto_measure_thickening_of_isClosed {α : Type u_1} [] {μ : } {s : Set α} (hs : R > 0, μ () ) (h's : ) :
Filter.Tendsto (fun (r : ) => μ ()) (nhdsWithin 0 ()) (nhds (μ s))

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

theorem measurable_edist {α : Type u_1} [] :
Measurable fun (p : α × α) => edist p.1 p.2
theorem Measurable.edist {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} (hf : ) (hg : ) :
Measurable fun (b : β) => edist (f b) (g b)
theorem AEMeasurable.edist {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} {μ : } (hf : ) (hg : ) :
AEMeasurable (fun (a : β) => edist (f a) (g a)) μ
theorem tendsto_measure_cthickening_of_isCompact {α : Type u_1} [] [] [] {μ : } {s : Set α} (hs : ) :
Filter.Tendsto (fun (r : ) => μ ()) (nhds 0) (nhds (μ s))

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

theorem exists_borelSpace_of_countablyGenerated_of_separatesPoints (α : Type u_5) [m : ] :
∃ (τ : ),

If a measurable space is countably generated and separates points, it arises as the borel sets of some second countable t4 topology (i.e. a separable metrizable one).

theorem exists_opensMeasurableSpace_of_countablySeparated (α : Type u_5) [m : ] :
∃ (τ : ),

If a measurable space on α is countably generated and separates points, there is some second countable t4 topology on α (i.e. a separable metrizable one) for which every open set is measurable.

theorem measurable_norm {α : Type u_1} [] :
theorem Measurable.norm {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) :
Measurable fun (a : β) => f a
theorem AEMeasurable.norm {α : Type u_1} {β : Type u_2} [] [] {f : βα} {μ : } (hf : ) :
AEMeasurable (fun (a : β) => f a) μ
theorem measurable_nnnorm {α : Type u_1} [] :
Measurable nnnorm
theorem Measurable.nnnorm {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) :
Measurable fun (a : β) => f a‖₊
theorem AEMeasurable.nnnorm {α : Type u_1} {β : Type u_2} [] [] {f : βα} {μ : } (hf : ) :
AEMeasurable (fun (a : β) => f a‖₊) μ
theorem measurable_ennnorm {α : Type u_1} [] :
Measurable fun (x : α) => x‖₊
theorem Measurable.ennnorm {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) :
Measurable fun (a : β) => f a‖₊
theorem AEMeasurable.ennnorm {α : Type u_1} {β : Type u_2} [] [] {f : βα} {μ : } (hf : ) :
AEMeasurable (fun (a : β) => f a‖₊) μ