EntropyPair.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The output of the concrete counterexample construction

Every field below concerns the actual finite-dimensional body, its literal cube and polar, or their covering numbers. The construction theorem supplies this record from only the numerical inputs a, r, and B.

def OAI.MetricEntropyDuality.entropyRatio line 23
Source documentation
The actual quotient of dual covering entropy by primal covering entropy.
```
def entropyRatio {ι : Type uι} [Fintype ι] (a : ℝ)
    (K : Set (RealSpace ι)) : ℝ :=
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace
def OAI.MetricEntropyDuality.entropyBudget line 29
Source documentation
The scalar upper bound, with radius and pivot count fixed by a alone.
```
def entropyBudget (a : ℝ) (r : ℕ) (B : ℝ) : ℝ :=
…
```
structure OAI.MetricEntropyDuality.EntropyPair line 35
Source documentation
A constructed body with its actual geometric and entropy properties. No matrix, compression theorem, or abstract entropy function is a field.
```
structure EntropyPair (a : ℝ) (r : ℕ) (B : ℝ) where
…
```