HasBoundedCoveringNumber

structure HasBoundedCoveringNumber {T : Type u_1} [PseudoEMetricSpace T] (A : Set T) (c : ENNReal) (d : ℝ) : Prop

A set A in a pseudoemetric space has bounded covering number with constant c and exponent d if it has finite diameter and for all ε ∈ (0, diam(A)], the covering number of A at scale ε is bounded by c * ε^{-d}.

• ediam_lt_top : EMetric.diam A < ⊤
• coveringNumber_le (ε : NNReal) : ↑ε ≤ EMetric.diam A → ↑(Metric.coveringNumber ε A) ≤ c * (↑ε)⁻¹ ^ d

theorem HasBoundedCoveringNumber.coveringNumber_lt_top {T : Type u_1} [PseudoEMetricSpace T] {A : Set T} {c : ENNReal} {ε : NNReal} {d : ℝ} (h : HasBoundedCoveringNumber A c d) (hε_ne : ε ≠ 0) (hc : c ≠ ⊤) (hd : 0 ≤ d) : Metric.coveringNumber ε A < ⊤

theorem HasBoundedCoveringNumber.subset {T : Type u_1} [PseudoEMetricSpace T] {A : Set T} {c : ENNReal} {d : ℝ} {B : Set T} (h : HasBoundedCoveringNumber A c d) (hBA : B ⊆ A) (hd : 0 ≤ d) : HasBoundedCoveringNumber B (2 ^ d * c) d

structure IsCoverWithBoundedCoveringNumber {T : Type u_1} [PseudoEMetricSpace T] (C : ℕ → Set T) (A : Set T) (c : ℕ → ENNReal) (d : ℕ → ℝ) : Prop

• c_ne_top (n : ℕ) : c n ≠ ⊤
• d_pos (n : ℕ) : 0 < d n
• isOpen (n : ℕ) : IsOpen (C n)
• totallyBounded (n : ℕ) : TotallyBounded (C n)
• hasBoundedCoveringNumber (n : ℕ) : HasBoundedCoveringNumber (C n) (c n) (d n)
• mono (n m : ℕ) : n ≤ m → C n ⊆ C m
• subset_iUnion : A ⊆ ⋃ (i : ℕ), C i

theorem isCoverWithBoundedCoveringNumber_Ico_nnreal : IsCoverWithBoundedCoveringNumber (fun (n : ℕ) => Set.Ico 0 (↑n + 1)) Set.univ (fun (n : ℕ) => 3 * (↑n + 1)) fun (x : ℕ) => 1