Metric entropy theorem statement specifications

This module records typechecked Prop targets for covering, packing, and epsilon-net results. These are specifications only, not proved theorems.

Verified Wikipedia reference: https://en.wikipedia.org/wiki/Covering_number

@[reducible, inline]

abbrev HighDimProb.maximalSeparatedNetStatement {alpha : Type u_1} [PseudoMetricSpace alpha] (K N : Set alpha) (eps : ℝ) : Prop

Statement target: a maximal epsilon-separated subset of K is an internal epsilon-net for K.

@[reducible, inline]

abbrev HighDimProb.epsilonNetCoveringNumberStatement {alpha : Type u_1} [PseudoMetricSpace alpha] (K N : Set alpha) (eps : ℝ) : Prop

Statement target: an internal epsilon-net gives an upper bound for the covering number by its cardinality.

Formula reference: an explicit epsilon-net bounds the covering number by the number of centers; see https://en.wikipedia.org/wiki/Covering_number

@[reducible, inline]

abbrev HighDimProb.packingCoveringInequalityStatement {alpha : Type u_1} [PseudoMetricSpace alpha] (K : Set alpha) (eps : ℝ) : Prop

Statement target: packing and covering numbers bound each other at related radii.

Formula reference: packing-covering comparisons are standard metric entropy estimates based on epsilon-separated sets and epsilon-covers; see https://en.wikipedia.org/wiki/Covering_number