MeanFourier.Mathlib.Topology.MetricSpace.CoveringNumbers

source

theorem Metric.le_coveringNumber_iff {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : NNReal} {n : ℕ∞} :

n ≤ coveringNumber ε s ↔ ∀ C ⊆ s, IsCover ε s C → n ≤ C.encard

source

theorem Metric.packingNumber_le_iff {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : NNReal} {n : ℕ∞} :

packingNumber ε s ≤ n ↔ ∀ P ⊆ s, IsSeparated (↑ε) P → P.encard ≤ n

source

@[simp]

theorem Metric.one_le_coveringNumber_iff {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : NNReal} :

1 ≤ coveringNumber ε s ↔ s.Nonempty

source

theorem Metric.coveringNumber_ne_zero_iff {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : NNReal} :

coveringNumber ε s ≠ 0 ↔ s.Nonempty

source

@[simp]

theorem Metric.one_le_externalCoveringNumber_iff {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : NNReal} :

1 ≤ externalCoveringNumber ε s ↔ s.Nonempty

source

theorem Metric.externalCoveringNumber_ne_zero_iff {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : NNReal} :

externalCoveringNumber ε s ≠ 0 ↔ s.Nonempty

source

@[simp]

theorem Metric.one_le_packingNumber_iff {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : NNReal} :

1 ≤ packingNumber ε s ↔ s.Nonempty

source

theorem Metric.packingNumber_ne_zero_iff {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : NNReal} :

packingNumber ε s ≠ 0 ↔ s.Nonempty

source

@[simp]

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

A.Nonempty → 0 < coveringNumber ε A

Alias of the reverse direction of Metric.coveringNumber_pos_iff.

source

@[simp]

theorem Metric.coveringNumber_ne_zero {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : NNReal} :

s.Nonempty → coveringNumber ε s ≠ 0

Alias of the reverse direction of Metric.coveringNumber_ne_zero_iff.

source

@[simp]

theorem Metric.one_le_coveringNumber {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : NNReal} :

s.Nonempty → 1 ≤ coveringNumber ε s

Alias of the reverse direction of Metric.one_le_coveringNumber_iff.

source

@[simp]

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

A.Nonempty → 0 < externalCoveringNumber ε A

Alias of the reverse direction of Metric.externalCoveringNumber_pos_iff.

source

@[simp]

theorem Metric.externalCoveringNumber_ne_zero {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : NNReal} :

s.Nonempty → externalCoveringNumber ε s ≠ 0

Alias of the reverse direction of Metric.externalCoveringNumber_ne_zero_iff.

source

@[simp]

theorem Metric.one_le_externalCoveringNumber {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : NNReal} :

s.Nonempty → 1 ≤ externalCoveringNumber ε s

Alias of the reverse direction of Metric.one_le_externalCoveringNumber_iff.

source

@[simp]

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

A.Nonempty → 0 < packingNumber ε A

Alias of the reverse direction of Metric.packingNumber_pos_iff.

source

@[simp]

theorem Metric.packingNumber_ne_zero {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : NNReal} :

s.Nonempty → packingNumber ε s ≠ 0

Alias of the reverse direction of Metric.packingNumber_ne_zero_iff.

source

@[simp]

theorem Metric.one_le_packingNumber {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : NNReal} :

s.Nonempty → 1 ≤ packingNumber ε s

Alias of the reverse direction of Metric.one_le_packingNumber_iff.

source

theorem Metric.packingNumber_two_mul_le_coveringNumber {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : NNReal} :

packingNumber (2 * ε) s ≤ coveringNumber ε s

source

theorem Metric.packingNumber_le_packingNumber_of_antilipschitzWith {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {f : X → Y} {s : Set X} {t : Set Y} {K ε : NNReal} (hst : Set.MapsTo f s t) (hf : AntilipschitzWith K f) :

packingNumber (K * ε) s ≤ packingNumber ε t

The smallness of the packing number is quantitatively pulled back under antilipschitz maps.

source

theorem Metric.coveringNumber_le_coveringNumber_of_antilipschitzWith {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {f : X → Y} {s : Set X} {t : Set Y} {K ε : NNReal} (hst : Set.MapsTo f s t) (hf : AntilipschitzWith K f) :

coveringNumber (2 * K * ε) s ≤ coveringNumber ε t

The smallness of the covering number is quantitatively pulled back under antilipschitz maps.

source

theorem Metric.coveringNumber_le_coveringNumber_of_lipschitzOnWith {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {f : X → Y} {s : Set X} {t : Set Y} {K ε : NNReal} (hst : Set.SurjOn f s t) (hst' : Set.MapsTo f s t) (hf : LipschitzOnWith K f s) :

coveringNumber (K * ε) t ≤ coveringNumber ε s

The smallness of the covering number is quantitatively pushed forward under surjective lipschitz maps.

source

theorem Metric.packingNumber_le_packingNumber_of_lipschitzOnWith {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {f : X → Y} {s : Set X} {t : Set Y} {K ε : NNReal} (hst : Set.SurjOn f s t) (hst' : Set.MapsTo f s t) (hf : LipschitzOnWith K f s) :

packingNumber (2 * K * ε) t ≤ packingNumber ε s

The smallness of the covering number is quantitatively pushed forward under surjective lipschitz maps.

source

theorem Metric.coveringNumber_prod_le {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {s : Set X} {t : Set Y} {ε : NNReal} :

coveringNumber ε (s ×ˢ t) ≤ coveringNumber ε s * coveringNumber ε t

source

theorem Metric.packingNumber_prod_le {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {s : Set X} {t : Set Y} {ε : NNReal} :

packingNumber ε (s ×ˢ t) ≤ packingNumber (ε / 2) s * packingNumber (ε / 2) t

source

theorem Metric.externalCoveringNumber_prod_le {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {s : Set X} {t : Set Y} {ε : NNReal} :

externalCoveringNumber ε (s ×ˢ t) ≤ externalCoveringNumber (ε / 2) s * externalCoveringNumber (ε / 2) t

source

theorem Metric.coveringNumber_pi_univ_le {ε : NNReal} {ι : Type u_3} [Fintype ι] {X : ι → Type u_4} [(i : ι) → PseudoEMetricSpace (X i)] {s : (i : ι) → Set (X i)} :

coveringNumber ε (Set.univ.pi s) ≤ ∏ i : ι, coveringNumber ε (s i)

source

theorem Metric.packingNumber_pi_univ_le {ε : NNReal} {ι : Type u_3} [Fintype ι] {X : ι → Type u_4} [(i : ι) → PseudoEMetricSpace (X i)] {s : (i : ι) → Set (X i)} :

packingNumber ε (Set.univ.pi s) ≤ ∏ i : ι, packingNumber (ε / 2) (s i)

source

theorem Metric.externalCoveringNumber_pi_univ_le {ε : NNReal} {ι : Type u_3} [Fintype ι] {X : ι → Type u_4} [(i : ι) → PseudoEMetricSpace (X i)] {s : (i : ι) → Set (X i)} :

externalCoveringNumber ε (Set.univ.pi s) ≤ ∏ i : ι, externalCoveringNumber (ε / 2) (s i)