SelectorProfile.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Exact counts in a selector profile

The full profile records each strict downward move by its final and original colors. These counting identities hold even without a global Earlier hypothesis: every point counted by a crossing already moves downward.

theorem OAI.TalagrandThreshold.Selector.profile_eq_card_filter_movedRow line 23
Source documentation
A profile entry is the original-color fiber within its moved row.
```
theorem profile_eq_card_filter_movedRow (a z : Coloring α s)
    (i : Fin s) (h : Color s) :
    profile a z i h = ((movedRow a z i).filter fun x => a x = h).card := by
…
```
Mentions: OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Color, OAI.TalagrandThreshold.Selector.profile, OAI.TalagrandThreshold.Selector.movedRow
theorem OAI.TalagrandThreshold.Selector.rowCount_profile line 38
Source documentation
All original colors partition the moved row.
```
theorem rowCount_profile (a z : Coloring α s) (i : Fin s) :
    rowCount (profile a z) i = (movedRow a z i).card := by
…
```
Mentions: OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.rowCount, OAI.TalagrandThreshold.Selector.profile, OAI.TalagrandThreshold.Selector.movedRow
theorem OAI.TalagrandThreshold.Selector.movedRow_card_eq_rowCount line 46
theorem OAI.TalagrandThreshold.Selector.movedRow_subset_changes line 51
theorem OAI.TalagrandThreshold.Selector.changes_filter_last line 60
Source documentation
The last color cannot be the final color of a strict downward move.
```
theorem changes_filter_last (a z : Coloring α s) :
    (changes a z).filter (fun x => z x = Fin.last s) = ∅ := by
…
```
Mentions: OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.changes
theorem OAI.TalagrandThreshold.Selector.changes_filter_castSucc line 73
Source documentation
The nonterminal final-color fibers are exactly the moved rows.
```
theorem changes_filter_castSucc (a z : Coloring α s) (i : Fin s) :
    (changes a z).filter (fun x => z x = i.castSucc) = movedRow a z i := by
…
```
Mentions: OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.changes, OAI.TalagrandThreshold.Selector.movedRow
theorem OAI.TalagrandThreshold.Selector.profileSize_profile line 85
Source documentation
Every changed point has exactly one nonterminal final color.
```
theorem profileSize_profile (a z : Coloring α s) :
    profileSize (profile a z) = (changes a z).card := by
…
```
Mentions: OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.profileSize, OAI.TalagrandThreshold.Selector.profile, OAI.TalagrandThreshold.Selector.changes
theorem OAI.TalagrandThreshold.Selector.profileSize_profile_eq_card_changes line 98
theorem OAI.TalagrandThreshold.Selector.profile_eq_zero_of_le line 104
Source documentation
Entries on or below the diagonal vanish in every actual profile.
```
theorem profile_eq_zero_of_le (a z : Coloring α s) (i : Fin s)
    (h : Color s) (hhi : h.val ≤ i.val) : profile a z i h = 0 := by
…
```
Mentions: OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Color, OAI.TalagrandThreshold.Selector.profile
theorem OAI.TalagrandThreshold.Selector.crossings_eq_profileCrossings line 109
Source documentation
The full profile determines every actual crossing count.
```
theorem crossings_eq_profileCrossings (a z : Coloring α s) (i : Fin s) :
    crossings a z i = profileCrossings (profile a z) i := by
…
```
Mentions: OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.crossings, OAI.TalagrandThreshold.Selector.profileCrossings, OAI.TalagrandThreshold.Selector.profile
theorem OAI.TalagrandThreshold.Selector.crossings_eq_of_profile_eq line 176
theorem OAI.TalagrandThreshold.Selector.rowCount_le_profileSize line 182
Source documentation
A row is bounded by the total size of any natural-valued profile.
```
theorem rowCount_le_profileSize (n : Profile s) (i : Fin s) :
    rowCount n i ≤ profileSize n := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.Profile, OAI.TalagrandThreshold.Selector.rowCount, OAI.TalagrandThreshold.Selector.profileSize
theorem OAI.TalagrandThreshold.Selector.profileCrossings_le_profileSize line 188
Source documentation
Restricting to entries crossing one level cannot increase total size.
```
theorem profileCrossings_le_profileSize (n : Profile s) (i : Fin s) :
    profileCrossings n i ≤ profileSize n := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.Profile, OAI.TalagrandThreshold.Selector.profileCrossings, OAI.TalagrandThreshold.Selector.profileSize
theorem OAI.TalagrandThreshold.Selector.crossings_le_card_changes line 197
theorem OAI.TalagrandThreshold.Selector.mem_groupOriginals line 202