Covering and packing numbers #

References #

Vershynin, High-Dimensional Probability (section 4.2)

def IsCover {E : Type u_1} [EDist E] (C : Set E) (ε : ENNReal) (A : Set E) :

A set C is an r-cover of another set A if every point in A belongs to a ball with radius r around a point of C.

Equations

IsCover C ε A = ∀ a ∈ A, ∃ c ∈ C, edist a c ≤ ε

Instances For

source

noncomputable def externalCoveringNumber {E : Type u_1} [EDist E] (r : ENNReal) (A : Set E) :

ℕ∞

Equations

externalCoveringNumber r A = ⨅ (C : Finset E), ⨅ (_ : IsCover (↑C) r A), ↑C.card

Instances For

source

noncomputable def internalCoveringNumber {E : Type u_1} [EDist E] (r : ENNReal) (A : Set E) :

ℕ∞

Equations

internalCoveringNumber r A = ⨅ (C : Finset E), ⨅ (_ : ↑C ⊆ A), ⨅ (_ : IsCover (↑C) r A), ↑C.card

Instances For

source

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

ℕ∞

Equations

packingNumber r A = ⨆ (C : Finset E), ⨆ (_ : ↑C ⊆ A), ⨆ (_ : Metric.IsSeparated r ↑C), ↑C.card

Instances For

source

theorem internalCoveringNumber_le_of_isCover {E : Type u_1} [EDist E] {C : Finset E} {r : ENNReal} {A : Set E} (C_sub : ↑C ⊆ A) (C_cov : IsCover (↑C) r A) :

internalCoveringNumber r A ≤ ↑C.card

source

@[simp]

theorem IsCover.self {E : Type u_1} [PseudoEMetricSpace E] (A : Set E) (r : ENNReal) :

IsCover A r A

source

theorem isCover_zero_iff {E : Type u_1} [EMetricSpace E] (C A : Set E) :

IsCover C 0 A ↔ A ⊆ C

source

theorem Set.Finite.internalCoveringNumber_le_ncard {E : Type u_1} [PseudoEMetricSpace E] (r : ENNReal) (A : Set E) (ha : A.Finite) :

internalCoveringNumber r A ≤ ↑A.ncard

source

@[simp]

theorem internalCoveringNumber_zero {E : Type u_1} [EMetricSpace E] (A : Set E) :

internalCoveringNumber 0 A = A.encard

source

theorem EMetric.isCover_iff {E : Type u_1} [PseudoEMetricSpace E] {C : Set E} {ε : ENNReal} {A : Set E} :

IsCover C ε A ↔ A ⊆ ⋃ x ∈ C, closedBall x ε

source

theorem isCover_empty_iff {E : Type u_1} [EDist E] (ε : ENNReal) (A : Set E) :

IsCover ∅ ε A ↔ A = ∅

source

theorem isCover_empty {E : Type u_1} [EDist E] (ε : ENNReal) :

IsCover ∅ ε ∅

source

theorem Set.Nonempty.one_le_internalCoveringNumber {E : Type u_1} [EDist E] {A : Set E} (hA : A.Nonempty) (r : ENNReal) :

1 ≤ internalCoveringNumber r A

source

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

internalCoveringNumber ⊤ A = 1

source

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

¬IsCover ∅ ε A

source

@[simp]

theorem internalCoveringNumber_empty {E : Type u_1} [EDist E] (r : ENNReal) :

internalCoveringNumber r ∅ = 0

source

@[simp]

theorem externalCoveringNumber_empty {E : Type u_1} [EDist E] (r : ENNReal) :

externalCoveringNumber r ∅ = 0

source

@[simp]

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

packingNumber r ∅ = 0

source

@[simp]

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

packingNumber r {x} = 1

source

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

IsCover {a} ε A

source

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

IsCover (↑{a}) ε A

source

theorem IsCover.mono {E : Type u_1} [EDist E] {C : Set E} {ε ε' : ENNReal} {A : Set E} (h : ε ≤ ε') (hC : IsCover C ε A) :

IsCover C ε' A

source

theorem IsCover.subset {E : Type u_1} [EDist E] {C : Set E} {ε : ENNReal} {A B : Set E} (h : A ⊆ B) (hC : IsCover C ε B) :

IsCover C ε A

source

theorem internalCoveringNumber_anti {E : Type u_1} [EDist E] {r r' : ENNReal} {A : Set E} (h : r ≤ r') :

internalCoveringNumber r' A ≤ internalCoveringNumber r A

source

theorem internalCoveringNumber_eq_one_of_diam_le {E : Type u_1} [PseudoEMetricSpace E] {r : ENNReal} {A : Set E} (h_nonempty : A.Nonempty) (hA : EMetric.diam A ≤ r) :

internalCoveringNumber r A = 1

source

theorem externalCoveringNumber_eq_one_of_diam_le {E : Type u_1} [PseudoEMetricSpace E] {r : ENNReal} {A : Set E} (h_nonempty : A.Nonempty) (hA : EMetric.diam A ≤ r) :

externalCoveringNumber r A = 1

source

theorem internalCoveringNumber_le_one_of_diam_le {E : Type u_1} [PseudoEMetricSpace E] {r : ENNReal} {A : Set E} (hA : EMetric.diam A ≤ r) :

internalCoveringNumber r A ≤ 1

source

@[simp]

theorem internalCoveringNumber_singleton {E : Type u_1} [PseudoEMetricSpace E] {x : E} {r : ENNReal} :

internalCoveringNumber r {x} = 1

source

@[simp]

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

externalCoveringNumber r {x} = 1

source

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

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

source

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

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

source

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

C.Nonempty

source

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

∃ (C : Finset E), ↑C ⊆ A ∧ IsCover (↑C) r A ∧ ↑C.card = internalCoveringNumber r A

source

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

Finset 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 : ENNReal} {A : Set E} (hr : 0 < r) :

↑(minimalCover r A hr) ⊆ A

source

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

IsCover (↑(minimalCover r A hr)) r A

source

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

↑(minimalCover r A hr).card = internalCoveringNumber r A

source

theorem exists_finset_card_eq_packingNumber {E : Type u_1} {r : ENNReal} {A : Set E} [PseudoEMetricSpace E] (h : packingNumber r A < ⊤) :

∃ (C : Finset E), ↑C ⊆ A ∧ Metric.IsSeparated r ↑C ∧ ↑C.card = packingNumber r A

source

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

Finset E

A maximal r-separated finite subset of A.

Equations

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

Instances For

source

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

↑(maximalSeparatedSet r A) ⊆ A

source

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

Metric.IsSeparated r ↑(maximalSeparatedSet r A)

source

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

↑(maximalSeparatedSet r A).card = packingNumber r A

source

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

C.card ≤ (maximalSeparatedSet r A).card

source

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

IsCover (↑(maximalSeparatedSet r A)) r A

source

theorem internalCoveringNumber_le_packingNumber {E : Type u_1} [PseudoEMetricSpace E] (r : ENNReal) (A : Set E) :

internalCoveringNumber r A ≤ packingNumber r A

source

theorem packingNumber_two_le_externalCoveringNumber {E : Type u_1} [PseudoEMetricSpace E] {r : ENNReal} (A : Set E) (hr : r ≠ ⊤) :

packingNumber (2 * r) A ≤ externalCoveringNumber r A

source

theorem externalCoveringNumber_le_internalCoveringNumber {E : Type u_1} [EDist E] (r : ENNReal) (A : Set E) :

externalCoveringNumber r A ≤ internalCoveringNumber r A

source

theorem internalCoveringNumber_two_le_externalCoveringNumber {E : Type u_1} [PseudoEMetricSpace E] (r : ENNReal) (A : Set E) :

internalCoveringNumber (2 * r) A ≤ externalCoveringNumber r A

source

theorem externalCoveringNumber_mono_set {E : Type u_1} [EDist E] {r : ENNReal} {A B : Set E} (h : A ⊆ B) :

externalCoveringNumber r A ≤ externalCoveringNumber r B

source

theorem internalCoveringNumber_subset_le {E : Type u_1} [PseudoEMetricSpace E] {r : ENNReal} (hr : r ≠ ⊤) {A B : Set E} (h : A ⊆ B) :

internalCoveringNumber r A ≤ internalCoveringNumber (r / 2) B

source

theorem internalCoveringNumber_le_encard {E : Type u_1} [PseudoEMetricSpace E] (r : ENNReal) {A : Set E} :

internalCoveringNumber r A ≤ A.encard

source

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

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

source

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

internalCoveringNumber r (f '' A) = internalCoveringNumber r A

source

theorem Isometry.internalCoveringNumber_image {E : Type u_1} {F : Type u_2} [EMetricSpace E] [PseudoEMetricSpace F] {f : E → F} (hf : Isometry f) {r : ENNReal} {A : Set E} :

internalCoveringNumber r (f '' A) = internalCoveringNumber r A

source

theorem internalCoveringNumber_Icc_zero_one_le_one_div {ε : ENNReal} (hε : ε ≤ 1) :

↑(internalCoveringNumber ε (Set.Icc 0 1)) ≤ 1 / ε

source

theorem volume_le_of_isCover {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {A : Set E} {C : Finset E} {ε : ENNReal} (hC : IsCover (↑C) ε A) :

MeasureTheory.volume A ≤ ↑C.card * 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] (A : Set E) {ε : ENNReal} (hε : 0 < ε) :

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

source

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

↑C.card * 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] (A : Set E) {ε : ENNReal} (hε : 0 < ε) (h : 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) (ε : ENNReal) :

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

Documentation

BrownianMotion.Continuity.CoveringNumber

Covering and packing numbers #

References #