Covering and packing numbers #

References #

Vershynin, High-Dimensional Probability (section 4.2)

noncomputable def Metric.externalCoveringNumber {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (A : Set X) :

The external covering number of a set A in X for radius ε is the minimal cardinality (in ℕ∞) of an ε-cover by points in X (not necessarily in A).

Equations

Metric.externalCoveringNumber ε A = ⨅ (C : Set X), ⨅ (_ : Metric.IsCover ε A C), C.encard

Instances For

source

noncomputable def Metric.coveringNumber {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (A : Set X) :

ℕ∞

The covering number (or internal covering number) of a set A for radius ε is the minimal cardinality (in ℕ∞) of an ε-cover contained in A.

Equations

Metric.coveringNumber ε A = ⨅ (C : Set X), ⨅ (_ : C ⊆ A), ⨅ (_ : Metric.IsCover ε A C), C.encard

Instances For

source

noncomputable def Metric.packingNumber {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (A : Set X) :

ℕ∞

The packing number of a set A for radius ε is the maximal cardinality (in ℕ∞) of an ε-separated set in A.

Equations

Metric.packingNumber ε A = ⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : Metric.IsSeparated (↑ε) C), C.encard

Instances For

source

@[simp]

theorem Metric.externalCoveringNumber_empty {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) :

externalCoveringNumber ε ∅ = 0

source

@[simp]

theorem Metric.coveringNumber_empty {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) :

coveringNumber ε ∅ = 0

source

@[simp]

theorem Metric.externalCoveringNumber_eq_zero {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} :

externalCoveringNumber ε A = 0 ↔ A = ∅

source

@[simp]

theorem Metric.externalCoveringNumber_pos {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} (hA : A.Nonempty) :

0 < externalCoveringNumber ε A

source

@[simp]

theorem Metric.coveringNumber_eq_zero {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} :

coveringNumber ε A = 0 ↔ A = ∅

source

@[simp]

theorem Metric.coveringNumber_pos {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} (hA : A.Nonempty) :

0 < coveringNumber ε A

source

theorem Metric.externalCoveringNumber_le_coveringNumber {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (A : Set X) :

externalCoveringNumber ε A ≤ coveringNumber ε A

source

theorem Metric.IsCover.externalCoveringNumber_le_encard {X : Type u_1} [PseudoEMetricSpace X] {A C : Set X} {ε : NNReal} (hC : IsCover ε A C) :

externalCoveringNumber ε A ≤ C.encard

source

theorem Metric.IsCover.coveringNumber_le_encard {X : Type u_1} [PseudoEMetricSpace X] {A C : Set X} {ε : NNReal} (h_subset : C ⊆ A) (hC : IsCover ε A C) :

coveringNumber ε A ≤ C.encard

source

theorem Metric.externalCoveringNumber_anti {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε δ : NNReal} (h : ε ≤ δ) :

externalCoveringNumber δ A ≤ externalCoveringNumber ε A

source

theorem Metric.coveringNumber_anti {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε δ : NNReal} (h : ε ≤ δ) :

coveringNumber δ A ≤ coveringNumber ε A

source

theorem Metric.externalCoveringNumber_mono_set {X : Type u_1} [PseudoEMetricSpace X] {A B : Set X} {ε : NNReal} (h : A ⊆ B) :

externalCoveringNumber ε A ≤ externalCoveringNumber ε B

source

theorem Metric.coveringNumber_eq_one_of_ediam_le {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} (h_nonempty : A.Nonempty) (hA : EMetric.diam A ≤ ↑ε) :

coveringNumber ε A = 1

source

theorem Metric.externalCoveringNumber_eq_one_of_ediam_le {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} (h_nonempty : A.Nonempty) (hA : EMetric.diam A ≤ ↑ε) :

externalCoveringNumber ε A = 1

source

theorem Metric.externalCoveringNumber_le_one_of_ediam_le {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} (hA : EMetric.diam A ≤ ↑ε) :

externalCoveringNumber ε A ≤ 1

source

theorem Metric.coveringNumber_le_one_of_ediam_le {X : Type u_1} [PseudoEMetricSpace X] {A : Set X} {ε : NNReal} (hA : EMetric.diam A ≤ ↑ε) :

coveringNumber ε A ≤ 1

source

theorem Metric.packingNumber_two_mul_le_externalCoveringNumber {X : Type u_1} [PseudoEMetricSpace X] (ε : NNReal) (A : Set X) :

packingNumber (2 * ε) A ≤ externalCoveringNumber ε A

The packing number of a set A for radius 2 * ε is at most the external covering number of A for radius ε.

source

@[simp]

theorem coveringNumber_zero {E : Type u_2} [EMetricSpace E] (A : Set E) :

Metric.coveringNumber 0 A = A.encard

source

theorem Set.Nonempty.one_le_coveringNumber {E : Type u_1} [PseudoEMetricSpace E] {A : Set E} (hA : A.Nonempty) (r : NNReal) :

1 ≤ Metric.coveringNumber r A

source

theorem not_isCover_empty {E : Type u_1} [PseudoEMetricSpace E] (ε : NNReal) (A : Set E) (h_nonempty : A.Nonempty) :

¬Metric.IsCover ε A ∅

source

@[simp]

theorem packingNumber_empty {E : Type u_1} [PseudoEMetricSpace E] (r : NNReal) :

Metric.packingNumber r ∅ = 0

source

@[simp]

theorem packingNumber_singleton {E : Type u_1} [PseudoEMetricSpace E] (r : NNReal) (x : E) :

Metric.packingNumber r {x} = 1

source

theorem isCover_singleton_finset_of_diam_le {E : Type u_1} [PseudoEMetricSpace E] {ε : NNReal} {A : Set E} {a : E} (hA : EMetric.diam A ≤ ↑ε) (ha : a ∈ A) :

Metric.IsCover ε A ↑{a}

source

@[simp]

theorem coveringNumber_singleton {E : Type u_1} [PseudoEMetricSpace E] {r : NNReal} {x : E} :

Metric.coveringNumber r {x} = 1

source

@[simp]

theorem externalCoveringNumber_singleton {E : Type u_1} [PseudoEMetricSpace E] {r : NNReal} {x : E} :

Metric.externalCoveringNumber r {x} = 1

source

theorem subset_iUnion_of_isCover {E : Type u_1} [PseudoEMetricSpace E] {ε : NNReal} {A C : Set E} (hC : Metric.IsCover ε A C) :

A ⊆ ⋃ x ∈ C, EMetric.closedBall x ↑ε

source

theorem TotallyBounded.exists_isCover {E : Type u_1} [PseudoEMetricSpace E] {A : Set E} (hA : TotallyBounded A) (r : NNReal) (hr : 0 < r) :

∃ (C : Finset E), ↑C ⊆ A ∧ Metric.IsCover r A ↑C

source

theorem IsCover.Nonempty {E : Type u_1} [PseudoEMetricSpace E] {ε : NNReal} {A C : Set E} (hC : Metric.IsCover ε A C) (hA : A.Nonempty) :

C.Nonempty

source

theorem exists_set_encard_eq_coveringNumber {E : Type u_1} [PseudoEMetricSpace E] {r : NNReal} {A : Set E} (h : TotallyBounded A) (hr : 0 < r) :

∃ C ⊆ A, C.Finite ∧ Metric.IsCover r A C ∧ C.encard = Metric.coveringNumber r A

source

noncomputable def minimalCover {E : Type u_1} [PseudoEMetricSpace E] (r : NNReal) (A : Set E) (hr : 0 < r) :

Set E

An internal r-cover of A with minimal cardinal.

Equations

minimalCover r A hr = if h : TotallyBounded A then ⋯.choose else ∅

Instances For

source

theorem minimalCover_subset {E : Type u_1} [PseudoEMetricSpace E] {r : NNReal} {A : Set E} (hr : 0 < r) :

minimalCover r A hr ⊆ A

source

theorem finite_minimalCover {E : Type u_1} [PseudoEMetricSpace E] {r : NNReal} {A : Set E} (hr : 0 < r) :

(minimalCover r A hr).Finite

source

theorem isCover_minimalCover {E : Type u_1} [PseudoEMetricSpace E] {r : NNReal} {A : Set E} (h : TotallyBounded A) (hr : 0 < r) :

Metric.IsCover r A (minimalCover r A hr)

source

theorem card_minimalCover {E : Type u_1} [PseudoEMetricSpace E] {r : NNReal} {A : Set E} (h : TotallyBounded A) (hr : 0 < r) :

(minimalCover r A hr).encard = Metric.coveringNumber r A

source

theorem exists_set_encard_eq_packingNumber {E : Type u_1} [PseudoEMetricSpace E] {r : NNReal} {A : Set E} (h : Metric.packingNumber r A < ⊤) :

∃ C ⊆ A, C.Finite ∧ Metric.IsSeparated (↑r) C ∧ C.encard = Metric.packingNumber r A

source

noncomputable def maximalSeparatedSet {E : Type u_1} [PseudoEMetricSpace E] (r : NNReal) (A : Set E) :

Set E

A maximal r-separated finite subset of A.

Equations

maximalSeparatedSet r A = if h : Metric.packingNumber r A < ⊤ then ⋯.choose else ∅

Instances For

source

theorem maximalSeparatedSet_subset {E : Type u_1} [PseudoEMetricSpace E] {r : NNReal} {A : Set E} :

maximalSeparatedSet r A ⊆ A

source

theorem isSeparated_maximalSeparatedSet {E : Type u_1} [PseudoEMetricSpace E] {r : NNReal} {A : Set E} :

Metric.IsSeparated (↑r) (maximalSeparatedSet r A)

source

theorem card_maximalSeparatedSet {E : Type u_1} [PseudoEMetricSpace E] {r : NNReal} {A : Set E} (h : Metric.packingNumber r A < ⊤) :

(maximalSeparatedSet r A).encard = Metric.packingNumber r A

source

theorem card_le_of_isSeparated {E : Type u_1} [PseudoEMetricSpace E] {r : NNReal} {A C : Set E} (h_subset : C ⊆ A) (h_sep : Metric.IsSeparated (↑r) C) (h : Metric.packingNumber r A < ⊤) :

C.encard ≤ (maximalSeparatedSet r A).encard

source

theorem isCover_maximalSeparatedSet {E : Type u_1} [PseudoEMetricSpace E] {r : NNReal} {A : Set E} (h : Metric.packingNumber r A < ⊤) :

Metric.IsCover r A (maximalSeparatedSet r A)

source

theorem coveringNumber_le_packingNumber {E : Type u_1} [PseudoEMetricSpace E] (r : NNReal) (A : Set E) :

Metric.coveringNumber r A ≤ Metric.packingNumber r A

source

theorem coveringNumber_two_le_externalCoveringNumber {E : Type u_1} [PseudoEMetricSpace E] (r : NNReal) (A : Set E) :

Metric.coveringNumber (2 * r) A ≤ Metric.externalCoveringNumber r A

source

theorem coveringNumber_subset_le {E : Type u_1} [PseudoEMetricSpace E] {r : NNReal} {A B : Set E} (h : A ⊆ B) :

Metric.coveringNumber r A ≤ Metric.coveringNumber (r / 2) B

source

theorem coveringNumber_le_encard {E : Type u_1} [PseudoEMetricSpace E] {A : Set E} (r : NNReal) :

Metric.coveringNumber r A ≤ A.encard

source

theorem Isometry.isCover_image_iff {E : Type u_1} [PseudoEMetricSpace E] {r : NNReal} {A : Set E} {F : Type u_2} [PseudoEMetricSpace F] {f : E → F} (hf : Isometry f) (C : Set E) :

Metric.IsCover r (f '' A) (f '' C) ↔ Metric.IsCover r A C

source

theorem Isometry.coveringNumber_image' {E : Type u_1} [PseudoEMetricSpace E] {r : NNReal} {A : Set E} {F : Type u_2} [PseudoEMetricSpace F] {f : E → F} (hf : Isometry f) (hf_inj : Set.InjOn f A) :

Metric.coveringNumber r (f '' A) = Metric.coveringNumber r A

source

theorem Isometry.coveringNumber_image {r : NNReal} {E : Type u_2} {F : Type u_3} [EMetricSpace E] [PseudoEMetricSpace F] {f : E → F} (hf : Isometry f) {A : Set E} :

Metric.coveringNumber r (f '' A) = Metric.coveringNumber r A

source

theorem coveringNumber_Icc_zero_one_le_one_div {ε : NNReal} (hε : ε ≤ 1) :

↑(Metric.coveringNumber ε (Set.Icc 0 1)) ≤ 1 / ↑ε

source

theorem EMetric.isCover_iff_subset_iUnion_closedBall {X : Type u_1} [PseudoEMetricSpace X] {ε : NNReal} {s N : Set X} :

Metric.IsCover ε s N ↔ s ⊆ ⋃ y ∈ N, closedBall y ↑ε

source

theorem volume_le_of_isCover {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ε : NNReal} {A C : Set E} (hC : Metric.IsCover ε A C) (hε : 0 < ε) :

MeasureTheory.volume A ≤ ↑C.encard * MeasureTheory.volume (EMetric.closedBall 0 ↑ε)

source

theorem volume_le_externalCoveringNumber_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ε : NNReal} (A : Set E) (hε : 0 < ε) :

MeasureTheory.volume A ≤ ↑(Metric.externalCoveringNumber ε A) * MeasureTheory.volume (EMetric.closedBall 0 ↑ε)

source

theorem le_volume_of_isSeparated_of_countable {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ε : NNReal} {A C : Set E} (hC_count : C.Countable) (hC : Metric.IsSeparated (↑ε) C) (h_subset : C ⊆ A) :

↑C.encard * MeasureTheory.volume (EMetric.closedBall 0 (↑ε / 2)) ≤ MeasureTheory.volume (A + EMetric.closedBall 0 (↑ε / 2))

source

theorem le_volume_of_isSeparated {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ε : NNReal} {A C : Set E} (hC : Metric.IsSeparated (↑ε) C) (h_subset : C ⊆ A) :

↑C.encard * MeasureTheory.volume (EMetric.closedBall 0 (↑ε / 2)) ≤ MeasureTheory.volume (A + EMetric.closedBall 0 (↑ε / 2))

source

theorem volume_eq_top_of_packingNumber {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ε : NNReal} (A : Set E) (hε : 0 < ε) (h : Metric.packingNumber ε A = ⊤) :

MeasureTheory.volume (A + EMetric.closedBall 0 (↑ε / 2)) = ⊤

source

theorem packingNumber_mul_le_volume {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (A : Set E) (ε : NNReal) :

↑(Metric.packingNumber ε A) * MeasureTheory.volume (EMetric.closedBall 0 (↑ε / 2)) ≤ MeasureTheory.volume (A + EMetric.closedBall 0 (↑ε / 2))

source

theorem volume_div_le_coveringNumber {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ε : NNReal} (A : Set E) (hε : 0 < ε) :

MeasureTheory.volume A / MeasureTheory.volume (EMetric.closedBall 0 ↑ε) ≤ ↑(Metric.coveringNumber ε A)

source

theorem coveringNumber_le_volume_div {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ε : NNReal} (A : Set E) (hε₁ : 0 < ε) :

↑(Metric.coveringNumber ε A) ≤ MeasureTheory.volume (A + EMetric.closedBall 0 (↑ε / 2)) / MeasureTheory.volume (EMetric.closedBall 0 (↑ε / 2))

source

theorem coveringNumber_closedBall_ge {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (ε : NNReal) (x : E) {r : NNReal} (hr : 0 < r) :

(↑r / ↑ε) ^ Module.finrank ℝ E ≤ ↑(Metric.coveringNumber ε (EMetric.closedBall x ↑r))

source

theorem coveringNumber_closedBall_one_ge {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (ε : NNReal) (x : E) :

(↑ε)⁻¹ ^ Module.finrank ℝ E ≤ ↑(Metric.coveringNumber ε (EMetric.closedBall x 1))

source

theorem coveringNumber_closedBall_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (ε : NNReal) (x : E) (r : NNReal) :

↑(Metric.coveringNumber ε (EMetric.closedBall x ↑r)) ≤ (2 * ↑r / ↑ε + 1) ^ Module.finrank ℝ E

source

theorem coveringNumber_closedBall_one_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (ε : NNReal) (x : E) :

↑(Metric.coveringNumber ε (EMetric.closedBall x 1)) ≤ (2 / ↑ε + 1) ^ Module.finrank ℝ E

source

theorem coveringNumber_closedBall_le_three_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ε : NNReal} [Nontrivial E] {x : E} {r : NNReal} (hr_zero : r ≠ 0) (hε : ε ≤ r) :

↑(Metric.coveringNumber ε (EMetric.closedBall x ↑r)) ≤ (3 * ↑r / ↑ε) ^ Module.finrank ℝ E

Documentation

BrownianMotion.Continuity.CoveringNumber

Covering and packing numbers #

References #