SelectorCountingEncodingRows.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Counting row encodings

A row encoding chooses a subset of the available positions and labels those positions with a word of a prescribed profile. The word count depends only on the number of chosen positions, so the total count factors into a binomial coefficient and the corresponding word count.

theorem OAI.TalagrandThreshold.card_fixedSize_subsets line 23

Source documentation

The number of subsets of R with exactly t elements.

theorem card_fixedSize_subsets (R : Finset α) (t : ℕ) :
    Fintype.card {U : Finset α // U ⊆ R ∧ U.card = t} =
      Nat.choose R.card t := by
…

def OAI.TalagrandThreshold.RowEncoding line 34
Source documentation
A chosen set of positions together with labels of the prescribed profile.
```
def RowEncoding (R : Finset α) (t : ℕ) (n : H → ℕ) : Type _ :=
…
```
instance OAI.TalagrandThreshold.instFintypeRowEncoding line 37
theorem OAI.TalagrandThreshold.card_rowEncoding line 43
Source documentation
Each chosen set admits the same number of words, so the count factors.
```
theorem card_rowEncoding (R : Finset α) (t : ℕ) (n : H → ℕ) :
    Fintype.card (RowEncoding R t n) = Nat.choose R.card t * wordCount t n := by
…
```
Mentions: OAI.TalagrandThreshold.RowEncoding, OAI.TalagrandThreshold.wordCount