CompressionCode.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Finite codes for uniform compression

A code records one common index, one label code for each level and pivot slot, and one weight code for each level, pivot slot, and subset of the index set. The decoded family is the actual image of this finite type under a fixed decoder. Its cardinality does not depend on the decoder's target type.

abbrev OAI.MetricEntropyDuality.CompressionCode line 20
Source documentation
The actual finite data retained by the compression construction.
```
abbrev CompressionCode (u q h s N : ℕ) :=
…
```
theorem OAI.MetricEntropyDuality.card_compressionCode line 25
Source documentation
Count the common index, label slots, and subset-weight slots exactly.
```
theorem card_compressionCode (u q h s N : ℕ) :
    Fintype.card (CompressionCode u q h s N) =
      u * q ^ (h * s) * N ^ (h * s * 2 ^ u) := by
…
```
Mentions: OAI.MetricEntropyDuality.CompressionCode
def OAI.MetricEntropyDuality.compressionImage line 38
Source documentation
Enumerate the actual image of the finite code space under a fixed decoder.
```
noncomputable def compressionImage (decode : CompressionCode u q h s N → E) : Finset E := by
…
```
Mentions: OAI.MetricEntropyDuality.CompressionCode
theorem OAI.MetricEntropyDuality.mem_compressionImage line 42
theorem OAI.MetricEntropyDuality.decode_mem_compressionImage line 47
theorem OAI.MetricEntropyDuality.card_compressionImage_le_code line 52
Source documentation
Collisions under decoding can only reduce the number of approximants.
```
theorem card_compressionImage_le_code (decode : CompressionCode u q h s N → E) :
    (compressionImage decode).card ≤ Fintype.card (CompressionCode u q h s N) := by
…
```
Mentions: OAI.MetricEntropyDuality.CompressionCode, OAI.MetricEntropyDuality.compressionImage
theorem OAI.MetricEntropyDuality.card_compressionImage_le line 59
theorem OAI.MetricEntropyDuality.compressionCode_nonempty line 67
Source documentation
Constant zero labels and weight codes work even if there are no levels or slots.
```
theorem compressionCode_nonempty (hu : 0 < u) (hq : 0 < q) (hN : 0 < N) :
    Nonempty (CompressionCode u q h s N) := by
…
```
Mentions: OAI.MetricEntropyDuality.CompressionCode
theorem OAI.MetricEntropyDuality.compressionImage_nonempty line 74
Source documentation
Decode an actual code to witness that the approximant family is nonempty.
```
theorem compressionImage_nonempty (decode : CompressionCode u q h s N → E)
    (hu : 0 < u) (hq : 0 < q) (hN : 0 < N) : (compressionImage decode).Nonempty := by
…
```
Mentions: OAI.MetricEntropyDuality.CompressionCode, OAI.MetricEntropyDuality.compressionImage