SelectorCountingWordsTransport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Transport of words with a prescribed profile

Reindexing the domain of a word preserves every letter count. Consequently, the number of words with a prescribed profile depends only on the size of the domain, including when that domain is the subtype of a finite set.

theorem OAI.TalagrandThreshold.wordProfile_comp_equiv line 21
Source documentation
A domain equivalence preserves the profile of a word.
```
theorem wordProfile_comp_equiv (e : D ≃ E) (f : E → H) :
    wordProfile (f ∘ e) = wordProfile f := by
…
```
Mentions: OAI.TalagrandThreshold.wordProfile
def OAI.TalagrandThreshold.wordFiberEquiv line 38
Source documentation
Reindexing gives an equivalence between words of the same profile.
```
def wordFiberEquiv (e : D ≃ E) (n : H → ℕ) :
    ↥(wordFiber D n) ≃ ↥(wordFiber E n) := by
…
```
Mentions: OAI.TalagrandThreshold.wordFiber
theorem OAI.TalagrandThreshold.wordFiber_card_eq_of_equiv line 52
Source documentation
Equivalent finite domains have equally many words of each profile.
```
theorem wordFiber_card_eq_of_equiv (e : D ≃ E) (n : H → ℕ) :
    (wordFiber D n).card = (wordFiber E n).card := by
…
```
Mentions: OAI.TalagrandThreshold.wordFiber
theorem OAI.TalagrandThreshold.wordFiber_card_eq_wordCount line 59
Source documentation
The word count on any finite domain agrees with the count on Fin.
```
theorem wordFiber_card_eq_wordCount (D : Type*) {H : Type*}
    [Fintype D] [DecidableEq D] [Fintype H] [DecidableEq H] (n : H → ℕ) :
    (wordFiber D n).card = wordCount (Fintype.card D) n := by
…
```
Mentions: OAI.TalagrandThreshold.wordFiber, OAI.TalagrandThreshold.wordCount
theorem OAI.TalagrandThreshold.wordFiber_finset_card line 66
Source documentation
Labels on a finite set are counted by the word count for its cardinality.
```
theorem wordFiber_finset_card {α H : Type*} [DecidableEq α]
    [Fintype H] [DecidableEq H] (U : Finset α) (n : H → ℕ) :
    (wordFiber ↥U n).card = wordCount U.card n := by
…
```
Mentions: OAI.TalagrandThreshold.wordFiber, OAI.TalagrandThreshold.wordCount