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}
[PseudoMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
{x : α}
{ε : ℝ}
:
MeasurableSet (Metric.ball x ε)
theorem
measurableSet_closedBall
{α : Type u_1}
[PseudoMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
{x : α}
{ε : ℝ}
:
theorem
measurable_infDist
{α : Type u_1}
[PseudoMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
{s : Set α}
:
Measurable fun (x : α) => Metric.infDist x s
theorem
Measurable.infDist
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
(hf : Measurable f)
{s : Set α}
:
Measurable fun (x : β) => Metric.infDist (f x) s
theorem
measurable_infNndist
{α : Type u_1}
[PseudoMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
{s : Set α}
:
Measurable fun (x : α) => Metric.infNndist x s
theorem
Measurable.infNndist
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
(hf : Measurable f)
{s : Set α}
:
Measurable fun (x : β) => Metric.infNndist (f x) s
theorem
measurable_dist
{α : Type u_1}
[PseudoMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
[SecondCountableTopology α]
:
Measurable fun (p : α × α) => dist p.1 p.2
theorem
Measurable.dist
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
[MeasurableSpace β]
[SecondCountableTopology α]
{f g : β → α}
(hf : Measurable f)
(hg : Measurable g)
:
Measurable fun (b : β) => dist (f b) (g b)
theorem
measurable_nndist
{α : Type u_1}
[PseudoMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
[SecondCountableTopology α]
:
Measurable fun (p : α × α) => nndist p.1 p.2
theorem
Measurable.nndist
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
[MeasurableSpace β]
[SecondCountableTopology α]
{f g : β → α}
(hf : Measurable f)
(hg : Measurable g)
:
Measurable fun (b : β) => nndist (f b) (g b)
theorem
measurableSet_eball
{α : Type u_1}
[PseudoEMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
{x : α}
{ε : ENNReal}
:
MeasurableSet (EMetric.ball x ε)
theorem
measurable_edist_right
{α : Type u_1}
[PseudoEMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
{x : α}
:
Measurable (edist x)
theorem
measurable_edist_left
{α : Type u_1}
[PseudoEMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
{x : α}
:
Measurable fun (y : α) => edist y x
theorem
measurable_infEdist
{α : Type u_1}
[PseudoEMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
{s : Set α}
:
Measurable fun (x : α) => EMetric.infEdist x s
theorem
Measurable.infEdist
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
(hf : Measurable f)
{s : Set α}
:
Measurable fun (x : β) => EMetric.infEdist (f x) s
theorem
tendsto_measure_cthickening
{α : Type u_1}
[PseudoEMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : ∃ R > 0, μ (Metric.cthickening R s) ≠ ⊤)
:
Filter.Tendsto (fun (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_isClosed
{α : Type u_1}
[PseudoEMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : ∃ R > 0, μ (Metric.cthickening R s) ≠ ⊤)
(h's : IsClosed s)
:
Filter.Tendsto (fun (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 closed
r-thickenings converge to its measure as r tends to 0.
theorem
tendsto_measure_thickening
{α : Type u_1}
[PseudoEMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : ∃ R > 0, μ (Metric.thickening R s) ≠ ⊤)
:
Filter.Tendsto (fun (r : ℝ) => μ (Metric.thickening r s)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (μ (closure s)))
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}
[PseudoEMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : ∃ R > 0, μ (Metric.thickening R s) ≠ ⊤)
(h's : IsClosed s)
:
Filter.Tendsto (fun (r : ℝ) => μ (Metric.thickening r s)) (nhdsWithin 0 (Set.Ioi 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}
[PseudoEMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
[SecondCountableTopology α]
:
Measurable fun (p : α × α) => edist p.1 p.2
theorem
Measurable.edist
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
[MeasurableSpace β]
[SecondCountableTopology α]
{f g : β → α}
(hf : Measurable f)
(hg : Measurable g)
:
Measurable fun (b : β) => edist (f b) (g b)
theorem
AEMeasurable.edist
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
[MeasurableSpace β]
[SecondCountableTopology α]
{f g : β → α}
{μ : MeasureTheory.Measure β}
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
:
AEMeasurable (fun (a : β) => edist (f a) (g a)) μ
theorem
tendsto_measure_cthickening_of_isCompact
{α : Type u_1}
[MetricSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
[ProperSpace α]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasureOnCompacts μ]
{s : Set α}
(hs : IsCompact s)
:
Filter.Tendsto (fun (r : ℝ) => μ (Metric.cthickening r s)) (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 : MeasurableSpace α]
[MeasurableSpace.CountablyGenerated α]
[MeasurableSpace.SeparatesPoints α]
:
∃ (x : TopologicalSpace α), SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α
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 : MeasurableSpace α]
[MeasurableSpace.CountablySeparated α]
:
∃ (x : TopologicalSpace α), SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α
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}
[MeasurableSpace α]
[NormedAddCommGroup α]
[OpensMeasurableSpace α]
:
Measurable norm
theorem
Measurable.norm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup α]
[OpensMeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
(hf : Measurable f)
:
Measurable fun (a : β) => ‖f a‖
theorem
AEMeasurable.norm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup α]
[OpensMeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
{μ : MeasureTheory.Measure β}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (a : β) => ‖f a‖) μ
theorem
measurable_nnnorm
{α : Type u_1}
[MeasurableSpace α]
[NormedAddCommGroup α]
[OpensMeasurableSpace α]
:
Measurable nnnorm
theorem
Measurable.nnnorm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup α]
[OpensMeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
(hf : Measurable f)
:
Measurable fun (a : β) => ‖f a‖₊
theorem
AEMeasurable.nnnorm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup α]
[OpensMeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
{μ : MeasureTheory.Measure β}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (a : β) => ‖f a‖₊) μ
theorem
measurable_ennnorm
{α : Type u_1}
[MeasurableSpace α]
[NormedAddCommGroup α]
[OpensMeasurableSpace α]
:
Measurable fun (x : α) => ↑‖x‖₊
theorem
Measurable.ennnorm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup α]
[OpensMeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
(hf : Measurable f)
:
Measurable fun (a : β) => ↑‖f a‖₊
theorem
AEMeasurable.ennnorm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup α]
[OpensMeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
{μ : MeasureTheory.Measure β}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (a : β) => ↑‖f a‖₊) μ