SelectorCountingWords.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Counting finite words by their color profiles

The coefficient attached to a profile is the actual cardinality of its fiber among finite words. Regrouping the weighted sum over words proves the finite multinomial identity without introducing a factorial formula or a counting hypothesis.

def OAI.TalagrandThreshold.wordProfile line 23
Source documentation
The number of positions of each color in a word on a finite domain.
```
def wordProfile {D H : Type*} [Fintype D] [DecidableEq H] (f : D → H) (h : H) : ℕ :=
…
```

def OAI.TalagrandThreshold.wordFiber line 27

Source documentation

All words on a fixed finite domain having the specified profile.

def wordFiber (D : Type*) {H : Type*} [Fintype D] [DecidableEq D]
    [Fintype H] [DecidableEq H] (n : H → ℕ) : Finset (D → H) :=
…

def OAI.TalagrandThreshold.wordCount line 32
Source documentation
The concrete multinomial coefficient, defined as a finite fiber cardinality.
```
def wordCount {H : Type*} [Fintype H] [DecidableEq H] (t : ℕ) (n : H → ℕ) : ℕ :=
…
```
def OAI.TalagrandThreshold.wordProfiles line 36
Source documentation
The finite set of profiles attained by words of length t.
```
def wordProfiles (H : Type*) [Fintype H] [DecidableEq H] (t : ℕ) : Finset (H → ℕ) :=
…
```
theorem OAI.TalagrandThreshold.mem_wordFiber line 41
theorem OAI.TalagrandThreshold.mem_wordProfiles_iff line 45
theorem OAI.TalagrandThreshold.sum_wordProfile line 49
theorem OAI.TalagrandThreshold.wordCount_eq_zero_of_not_mem_wordProfiles line 54
theorem OAI.TalagrandThreshold.prod_weight_wordProfile line 63
Source documentation
The weight from a profile equals the product of the individual letter weights.
```
theorem prod_weight_wordProfile {D : Type*} [Fintype D]
    (f : D → H) (π : H → ℝ) :
    (∏ h, π h ^ wordProfile f h) = ∏ i, π (f i) := by
…
```
Mentions: OAI.TalagrandThreshold.wordProfile
theorem OAI.TalagrandThreshold.sum_wordCount_weight line 70
Source documentation
The multinomial identity obtained by grouping actual words by their profile.
```
theorem sum_wordCount_weight (t : ℕ) (π : H → ℝ) :
    (∑ n ∈ wordProfiles H t, (wordCount t n : ℝ) * ∏ h, π h ^ n h) =
      (∑ h, π h) ^ t := by
…
```
Mentions: OAI.TalagrandThreshold.wordProfiles, OAI.TalagrandThreshold.wordCount
theorem OAI.TalagrandThreshold.wordCount_weight_nonneg line 86
theorem OAI.TalagrandThreshold.sum_wordCount_weight_le_one line 90
theorem OAI.TalagrandThreshold.sum_wordCount_weight_finset_le_one line 98
Source documentation
Any finite collection of profiles has total weight at most one, including profiles not attained by a word: their fiber counts are zero.
```
theorem sum_wordCount_weight_finset_le_one (t : ℕ) (E : Finset (H → ℕ))
    (π : H → ℝ) (hπ : ∀ h, 0 ≤ π h) (hπsum : (∑ h, π h) ≤ 1) :
    (∑ n ∈ E, (wordCount t n : ℝ) * ∏ h, π h ^ n h) ≤ 1 := by
…
```
Mentions: OAI.TalagrandThreshold.wordCount