Sets with bounded covering exponent

A property of sets in a pseudoemetric space that bounds the growth of their covering numbers as the radius of the balls goes to zero. This will be used in the proof of the Kolmogorov-Chentsov theorem, that gives a sufficient condition for a stochastic process to have a modification with Hölder continuous paths.

Main definitions

• HasCoveringExponent A c d : 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}.

Main statements

• HasCoveringExponent.subset: if A has bounded covering exponent with constant c and exponent d, then any subset of A has bounded covering exponent with constant 2^d * c and exponent d.

structure Metric.HasCoveringExponent {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 : ediam A < ⊤
• coveringNumber_le (ε : NNReal) : ↑ε ≤ ediam A → ↑(coveringNumber ε A) ≤ c * (↑ε)⁻¹ ^ d

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

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

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