SelectorCountingEncoding.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Reconstruction from the actual changed rows

For an earlier coloring, every point outside the changed rows retains its final color. Inside a changed row its original color is recorded. Thus the changed subsets and their original labels determine the entire original coloring.

theorem OAI.TalagrandThreshold.Selector.coloring_eq_of_movedRows line 22
Source documentation
An original coloring is reconstructed from its changed rows and the original labels on those rows. No disjointness of ambient row supersets is used.
```
theorem coloring_eq_of_movedRows
    {a b z : Coloring α s} (ha : Earlier a z) (hb : Earlier b z)
    (hrows : ∀ i, movedRow a z i = movedRow b z i)
    (hlabels : ∀ i x, x ∈ movedRow a z i → a x = b x) : a = b := by
…
```
Mentions: OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Earlier, OAI.TalagrandThreshold.Selector.movedRow
abbrev OAI.TalagrandThreshold.Selector.RawRowEncoding line 46
Source documentation
The unrestricted row record consists of its actual support and its labels.
```
abbrev RawRowEncoding (α : Type*) (s : ℕ) :=
…
```
def OAI.TalagrandThreshold.Selector.rawRowEncoding line 49
def OAI.TalagrandThreshold.Selector.rawRowLookup line 53
Source documentation
Reading one point avoids any dependence on the chosen subtype proof.
```
def rawRowLookup (E : RawRowEncoding α s) (x : α) : Option (Color s) :=
…
```
Mentions: OAI.TalagrandThreshold.Selector.RawRowEncoding, OAI.TalagrandThreshold.Color
theorem OAI.TalagrandThreshold.Selector.rawRowEncoding_injective line 57
Source documentation
The literal row encoding is injective on originals moved only earlier.
```
theorem rawRowEncoding_injective
    {a b z : Coloring α s} (ha : Earlier a z) (hb : Earlier b z)
    (he : ∀ i, rawRowEncoding a z i = rawRowEncoding b z i) : a = b := by
…
```
Mentions: OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Earlier, OAI.TalagrandThreshold.Selector.rawRowEncoding