SelectorCountingEncodingBound.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The fixed-profile encoding bound

Each actual coloring maps to the tuple of its changed row subsets and the original colors on them. Reconstruction proves this map injective. The row record permits arbitrary subsets of the fixed ambient sets, so overlap between those ambient sets can only enlarge the number of records.

theorem OAI.TalagrandThreshold.Selector.wordProfile_restrict_finset line 25
Source documentation
Restricting a labeling to a finite set counts exactly its fibers there.
```
theorem wordProfile_restrict_finset {H : Type*} [DecidableEq H]
    (U : Finset α) (f : α → H) (h : H) :
    wordProfile (fun x : ↥U => f x.val) h =
      (U.filter fun x => f x = h).card := by
…
```
Mentions: OAI.TalagrandThreshold.wordProfile
theorem OAI.TalagrandThreshold.Selector.movedRow_wordProfile line 41
Source documentation
The recorded original labels have precisely the actual profile row.
```
theorem movedRow_wordProfile (a z : Coloring α s) (i : Fin s) :
    wordProfile (fun x : ↥(movedRow a z i) => a x.val) = profile a z i := by
…
```
Mentions: OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.wordProfile, OAI.TalagrandThreshold.Selector.movedRow, OAI.TalagrandThreshold.Selector.profile
def OAI.TalagrandThreshold.Selector.profileRowEncoding line 47
Source documentation
The literal row record with its proved size and histogram constraints.
```
def profileRowEncoding (a z : Coloring α s) (n : Profile s)
    (R : Fin s → Finset α) (hn : profile a z = n)
    (hR : ∀ i, movedRow a z i ⊆ R i) (i : Fin s) :
    RowEncoding (R i) (rowCount n i) (n i) :=
…
```
Mentions: OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Profile, OAI.TalagrandThreshold.Selector.profile, OAI.TalagrandThreshold.Selector.movedRow, OAI.TalagrandThreshold.RowEncoding, OAI.TalagrandThreshold.Selector.rowCount
def OAI.TalagrandThreshold.Selector.rowEncodingForget line 56
Source documentation
Forgetting the constraints retains the actual changed subset and labels.
```
def rowEncodingForget {R : Finset α} {t : ℕ} {n : Color s → ℕ}
    (E : RowEncoding R t n) : RawRowEncoding α s :=
…
```
Mentions: OAI.TalagrandThreshold.Color, OAI.TalagrandThreshold.RowEncoding, OAI.TalagrandThreshold.Selector.RawRowEncoding
theorem OAI.TalagrandThreshold.Selector.rowEncodingForget_profileRowEncoding line 60
theorem OAI.TalagrandThreshold.Selector.card_le_profile_encoding line 68
Source documentation
Count actual originals of a fixed final coloring and profile. Every injectivity and histogram condition is proved from the actual row encoding.
```
theorem card_le_profile_encoding
    (G : Finset (Coloring α s)) (z : Coloring α s) (n : Profile s)
    (R : Fin s → Finset α)
    (hEarlier : ∀ a ∈ G, Earlier a z)
    (hprofile : ∀ a ∈ G, profile a z = n)
    (hrows : ∀ a ∈ G, ∀ i, movedRow a z i ⊆ R i) :
    G.card ≤ ∏ i : Fin s,
      Nat.choose (R i).card (rowCount n i) * wordCount (rowCount n i) (n i) := by
…
```
Mentions: OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Profile, OAI.TalagrandThreshold.Selector.Earlier, OAI.TalagrandThreshold.Selector.profile, OAI.TalagrandThreshold.Selector.movedRow, OAI.TalagrandThreshold.Selector.rowCount, OAI.TalagrandThreshold.wordCount
theorem OAI.TalagrandThreshold.Selector.groupOriginals_card_le_profile_encoding line 92
Source documentation
Specialization to the actual selected bad originals in one profile group.
```
theorem groupOriginals_card_le_profile_encoding
    {F : Family α} (mu : MassFamily F) (z : Coloring α s) (n : Profile s)
    (R : Fin s → Finset α)
    (hrows : ∀ a ∈ groupOriginals mu z n, ∀ i, movedRow a z i ⊆ R i) :
    (groupOriginals mu z n).card ≤ ∏ i : Fin s,
      Nat.choose (R i).card (rowCount n i) * wordCount (rowCount n i) (n i) := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Profile, OAI.TalagrandThreshold.Selector.groupOriginals, OAI.TalagrandThreshold.Selector.movedRow, OAI.TalagrandThreshold.Selector.rowCount, OAI.TalagrandThreshold.wordCount