Covers in a metric space

This file defines covers, aka nets, which are a quantitative notion of compactness in a metric space.

A ε-cover of a set s is a set N such that every element of s is at distance at most ε to some element of N.

In a proper metric space, sets admitting a finite cover are precisely the relatively compact sets.

References

R. Vershynin, High Dimensional Probability, Section 4.2.

instance Metric.instIsReflSetOfProdMatch_8PropLeENNRealEdistOfNNReal {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} : SetRel.IsRefl {(x, y) : X × X | edist x y ≤ ↑ε}

instance Metric.instIsSymmSetOfProdMatch_1PropLeENNRealEdistOfNNReal {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} : SetRel.IsSymm {(x, y) : X × X | edist x y ≤ ↑ε}

def Metric.IsCover {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (s N : Set X) : Prop

A set N is an ε-cover of a set s if every point of s lies at distance at most ε of some point of N.

This is also called an ε-net in the literature.

R. Vershynin, High Dimensional Probability, 4.2.1.

Equations

• Metric.IsCover ε s N = SetRel.IsCover {(x, y) : X × X | edist x y ≤ ↑ε} s N

@[simp]

theorem Metric.IsCover.empty {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} {N : Set X} : IsCover ε ∅ N

theorem Metric.IsCover.nonempty {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} {s N : Set X} (hsN : IsCover ε s N) (hs : s.Nonempty) : N.Nonempty

theorem Metric.IsCover.mono {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} {s N₁ N₂ : Set X} (hN : N₁ ⊆ N₂) (h₁ : IsCover ε s N₁) : IsCover ε s N₂

theorem Metric.IsCover.anti {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} {s t N : Set X} (hst : s ⊆ t) (ht : IsCover ε t N) : IsCover ε s N

theorem Metric.IsCover.mono_radius {X : Type u_1} [PseudoEMetricSpace X] {ε δ : NNReal} {s N : Set X} (hεδ : ε ≤ δ) (hε : IsCover ε s N) : IsCover δ s N

theorem Metric.isCover_iff_subset_iUnion_emetricClosedBall {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} {s N : Set X} : IsCover ε s N ↔ s ⊆ ⋃ y ∈ N, EMetric.closedBall y ↑ε

theorem Metric.IsCover.of_maximal_isSeparated {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} {s N : Set X} (hN : Maximal (fun (N : Set X) => N ⊆ s ∧ IsSeparated (↑ε) N) N) : IsCover ε s N

A maximal ε-separated subset of a set s is an ε-cover of s.

R. Vershynin, High Dimensional Probability, 4.2.6.

theorem Metric.isCover_iff_subset_iUnion_closedBall {X : Type u_1} [PseudoMetricSpace X] {ε : NNReal} {s N : Set X} : IsCover ε s N ↔ s ⊆ ⋃ y ∈ N, closedBall y ↑ε

theorem Metric.IsCover.subset_iUnion_closedBall {X : Type u_1} [PseudoMetricSpace X] {ε : NNReal} {s N : Set X} : IsCover ε s N → s ⊆ ⋃ y ∈ N, closedBall y ↑ε

Alias of the forward direction of Metric.isCover_iff_subset_iUnion_closedBall.

theorem Metric.IsCover.of_subset_iUnion_closedBall {X : Type u_1} [PseudoMetricSpace X] {ε : NNReal} {s N : Set X} : s ⊆ ⋃ y ∈ N, closedBall y ↑ε → IsCover ε s N

Alias of the reverse direction of Metric.isCover_iff_subset_iUnion_closedBall.

theorem Metric.exists_finite_isCover_of_isCompact_closure {X : Type u_1} [PseudoMetricSpace X] {ε : NNReal} {s : Set X} (hε : ε ≠ 0) (hs : IsCompact (closure s)) : ∃ N ⊆ s, N.Finite ∧ IsCover ε s N

A relatively compact set admits a finite cover.

theorem Metric.exists_finite_isCover_of_isCompact {X : Type u_1} [PseudoMetricSpace X] {ε : NNReal} {s : Set X} (hε : ε ≠ 0) (hs : IsCompact s) : ∃ N ⊆ s, N.Finite ∧ IsCover ε s N

A compact set admits a finite cover.

theorem Metric.IsCover.of_subset_cthickening_of_lt {X : Type u_1} [PseudoMetricSpace X] {ε : NNReal} {s N : Set X} {δ : NNReal} (hsN : s ⊆ cthickening (↑ε) N) (hεδ : ε < δ) : IsCover δ s N

theorem Metric.isCover_iff_subset_cthickening {X : Type u_1} [PseudoMetricSpace X] {ε : NNReal} {s N : Set X} [ProperSpace X] (hN : IsClosed N) : IsCover ε s N ↔ s ⊆ cthickening (↑ε) N

theorem Metric.IsCover.of_subset_cthickening {X : Type u_1} [PseudoMetricSpace X] {ε : NNReal} {s N : Set X} [ProperSpace X] (hN : IsClosed N) : s ⊆ cthickening (↑ε) N → IsCover ε s N

Alias of the reverse direction of Metric.isCover_iff_subset_cthickening.

theorem Metric.IsCover.subset_cthickening {X : Type u_1} [PseudoMetricSpace X] {ε : NNReal} {s N : Set X} [ProperSpace X] (hN : IsClosed N) : IsCover ε s N → s ⊆ cthickening (↑ε) N

Alias of the forward direction of Metric.isCover_iff_subset_cthickening.

@[simp]

theorem Metric.isCover_closure {X : Type u_1} [PseudoMetricSpace X] {ε : NNReal} {s N : Set X} [ProperSpace X] (hN : IsClosed N) : IsCover ε (closure s) N ↔ IsCover ε s N

theorem Metric.IsCover.closure {X : Type u_1} [PseudoMetricSpace X] {ε : NNReal} {s N : Set X} [ProperSpace X] (hN : IsClosed N) : IsCover ε s N → IsCover ε (closure s) N

Alias of the reverse direction of Metric.isCover_closure.

@[simp]

theorem Metric.isCover_zero {X : Type u_1} [EMetricSpace X] {s N : Set X} : IsCover 0 s N ↔ s ⊆ N

theorem Metric.IsCover.isCompact {X : Type u_1} [MetricSpace X] [ProperSpace X] {ε : NNReal} {s N : Set X} (hsN : IsCover ε s N) (hs : IsClosed s) (hN : IsCompact N) : IsCompact s

A closed set in a proper metric space which admits a compact cover is compact.

theorem Metric.IsCover.isCompact_closure {X : Type u_1} [MetricSpace X] [ProperSpace X] {ε : NNReal} {s N : Set X} (hsN : IsCover ε s N) (hN : IsCompact N) : IsCompact (closure s)

A set in a proper metric space which admits a compact cover is relatively compact.

theorem Metric.isCompact_closure_iff_exists_finite_isCover {X : Type u_1} [MetricSpace X] [ProperSpace X] {ε : NNReal} {s : Set X} (hε : ε ≠ 0) : IsCompact (closure s) ↔ ∃ N ⊆ s, N.Finite ∧ IsCover ε s N

A set in a proper metric space admits a finite cover iff it is relatively compact.

R. Vershynin, High Dimensional Probability, 4.2.3. Note that the print edition incorrectly claims that this holds without the ProperSpace X assumption.