LabelEncoding.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Fixed encodings of realized partition labels

Only the realized labels are counted. The ambient label types need not be finite, and representatives are fixed from the label maps alone, before any coefficient vector enters the compression construction.

structure OAI.MetricEntropyDuality.FixedLabels line 23
Source documentation
Shared finite label data for a family of partitions. A representative is defined at every code, including unused codes, and preserves each realized label when applied to its encoding.
```
structure FixedLabels {X : Type uX} {u : ℕ} {Label : Fin u → Type uLabel}
    (L : (i : Fin u) → X → Label i) (q : ℕ) where
…
```
def OAI.MetricEntropyDuality.FixedLabels.rangeEmbedding line 37
Source documentation
Embed the finite range, rather than the entire ambient label type.
```
def rangeEmbedding {Y : Type uY} [Finite X] (f : X → Y) (q : ℕ)
    (hcard : Nat.card (Set.range f) ≤ q) : Set.range f ↪ Fin q :=
…
```
def OAI.MetricEntropyDuality.FixedLabels.ofCardBound line 45
Source documentation
Construct all encodings and representative maps from the fixed label family and its realized-cardinality bounds. The construction has no measure or coefficient-vector parameter. Nonempty X supplies a representative even at codes outside the encoding's image.
```
def ofCardBound [Finite X] [Nonempty X]
    (L : (i : Fin u) → X → Label i)
    (hcard : ∀ i, Nat.card (Set.range (L i)) ≤ q) : FixedLabels L q := by
…
```
Mentions: OAI.MetricEntropyDuality.FixedLabels
theorem OAI.MetricEntropyDuality.FixedLabels.encode_representative_encode line 65
Source documentation
Replacing a vertex by its fixed representative keeps its finite code.
```
theorem encode_representative_encode (E : FixedLabels L q) (i : Fin u) (x : X) :
    E.encode i (E.representative i (E.encode i x)) = E.encode i x :=
…
```
Mentions: OAI.MetricEntropyDuality.FixedLabels
theorem OAI.MetricEntropyDuality.FixedLabels.representative_encode_eq_of_label_eq line 70
Source documentation
Equal labels select the same fixed representative.
```
theorem representative_encode_eq_of_label_eq (E : FixedLabels L q)
    (i : Fin u) {x y : X} (h : L i x = L i y) :
    E.representative i (E.encode i x) = E.representative i (E.encode i y) := by
…
```
Mentions: OAI.MetricEntropyDuality.FixedLabels
def OAI.MetricEntropyDuality.FixedLabels.paddingCode line 76
Source documentation
A fixed vertex supplies a realized code for padding unused pivot slots.
```
def paddingCode [Nonempty X] (E : FixedLabels L q) (i : Fin u) : Fin q :=
…
```
Mentions: OAI.MetricEntropyDuality.FixedLabels
theorem OAI.MetricEntropyDuality.FixedLabels.paddingCode_realized line 79