CompressionDecoder.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The fixed decoded family of compression approximants

The decoder uses only shared partition data, fixed label representatives, and the finite code. Original column centers and coefficient vectors are absent from its arguments. Every subset of the partition indices receives a weight slot, so the enumeration includes every admissible-family encoding.

def OAI.MetricEntropyDuality.compressionDecode line 30
Source documentation
Decode the common index, pivot labels, and rounded grouped weights into an actual real-valued function on the original domain.
```
def compressionDecode (L : (i : Fin u) → X → Label i) (E : FixedLabels L q)
    (h s : ℕ) (θ : ℝ)
    (code : CompressionCode u q h s (weightCodeSize (roundingStep θ s u))) : X → ℝ :=
…
```
Mentions: OAI.MetricEntropyDuality.FixedLabels, OAI.MetricEntropyDuality.CompressionCode, OAI.MetricEntropyDuality.weightCodeSize, OAI.MetricEntropyDuality.roundingStep
def OAI.MetricEntropyDuality.compressionList line 40
Source documentation
The actual finite family, fixed before choosing a coefficient vector.
```
def compressionList (L : (i : Fin u) → X → Label i) (E : FixedLabels L q)
    (h s : ℕ) (θ : ℝ) : Finset (X → ℝ) :=
…
```
Mentions: OAI.MetricEntropyDuality.FixedLabels
theorem OAI.MetricEntropyDuality.mem_compressionList line 44
theorem OAI.MetricEntropyDuality.compressionDecode_mem_compressionList line 52
Source documentation
Every encoded construction is included in the one shared finite list.
```
theorem compressionDecode_mem_compressionList
    (L : (i : Fin u) → X → Label i) (E : FixedLabels L q) (h s : ℕ) (θ : ℝ)
    (code : CompressionCode u q h s (weightCodeSize (roundingStep θ s u))) :
    compressionDecode L E h s θ code ∈ compressionList L E h s θ :=
…
```
Mentions: OAI.MetricEntropyDuality.FixedLabels, OAI.MetricEntropyDuality.CompressionCode, OAI.MetricEntropyDuality.weightCodeSize, OAI.MetricEntropyDuality.roundingStep, OAI.MetricEntropyDuality.compressionDecode, OAI.MetricEntropyDuality.compressionList
theorem OAI.MetricEntropyDuality.compressionList_nonempty line 60
Source documentation
The finite family is nonempty for positive index and label counts. The rounded-weight alphabet is always nonempty, even at degenerate meshes.
```
theorem compressionList_nonempty
    (L : (i : Fin u) → X → Label i) (E : FixedLabels L q) (h s : ℕ) (θ : ℝ)
    (hu : 0 < u) (hq : 0 < q) : (compressionList L E h s θ).Nonempty :=
…
```
Mentions: OAI.MetricEntropyDuality.FixedLabels, OAI.MetricEntropyDuality.compressionList
theorem OAI.MetricEntropyDuality.compressionList_card_le_nat line 66
Source documentation
First count with the exact integer size of the rounded-weight alphabet.
```
theorem compressionList_card_le_nat
    (L : (i : Fin u) → X → Label i) (E : FixedLabels L q) (h s : ℕ) (θ : ℝ) :
    (compressionList L E h s θ).card ≤
      u * q ^ (h * s) * weightCodeSize (roundingStep θ s u) ^ (h * s * 2 ^ u) :=
…
```
Mentions: OAI.MetricEntropyDuality.FixedLabels, OAI.MetricEntropyDuality.compressionList, OAI.MetricEntropyDuality.weightCodeSize, OAI.MetricEntropyDuality.roundingStep

theorem OAI.MetricEntropyDuality.compressionList_card_le line 74

Source documentation

The real cardinality bound, with no factor involving the size of X, original pivots, or column centers.

theorem compressionList_card_le
    (L : (i : Fin u) → X → Label i) (E : FixedLabels L q) (h s : ℕ) (θ : ℝ)
    (hθ : 0 < θ) (hs : 0 < s) :
    ((compressionList L E h s θ).card : ℝ) ≤
      (u : ℝ) * (q : ℝ) ^ (h * s) *
        (1 + (s : ℝ) * 2 ^ u / θ) ^ (h * s * 2 ^ u) := by
…

Mentions: OAI.MetricEntropyDuality.FixedLabels, OAI.MetricEntropyDuality.compressionList