SelectorGroupCost.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual contribution of one full selector profile

The common heavy sets are obtained separately for each occurring profile. The entropy estimate removes their sizes before profiles are summed, so no uniform choice of heavy sets across distinct profiles is required.

theorem OAI.TalagrandThreshold.Selector.profile_group_cost_le line 28
Source documentation
A finite group with a fixed final coloring and full profile has the claimed weighted contribution whenever its rows fit the actual heavy sets.
```
theorem profile_group_cost_le (p : ℝ) (s : ℕ) (hp : 0 < p)
    (hs : p * scaleSum s ≤ 1 / 2)
    (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)
    (hR : ∀ i, (R i).card ≤ 2 ^ (i.val + 1) * profileSize n) :
    (∑ a ∈ G, colorMass p s a * p ^ (changes a z).card) ≤
      colorMass p s z *
        (∏ i : Fin s, (3 / (64 : ℝ) ^ (i.val + 1)) ^ (rowCount n i)) *
        (∏ i : Fin s, ((wordCount (rowCount n i) (n i) : ℝ) *
…
```
Mentions: OAI.TalagrandThreshold.scaleSum, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Profile, OAI.TalagrandThreshold.Selector.Earlier, OAI.TalagrandThreshold.Selector.profile, OAI.TalagrandThreshold.Selector.movedRow, OAI.TalagrandThreshold.Selector.profileSize, OAI.TalagrandThreshold.colorMass, OAI.TalagrandThreshold.Selector.changes, OAI.TalagrandThreshold.Selector.rowCount, OAI.TalagrandThreshold.wordCount
theorem OAI.TalagrandThreshold.Selector.group_cost_le line 95
Source documentation
The contribution of an actual selected profile. All reconstruction and counting premises are discharged by the concrete selector construction.
```
theorem group_cost_le {F : Family α} (mu : MassFamily F)
    (p : ℝ) (s : ℕ) (hp : 0 < p) (hs : p * scaleSum s ≤ 1 / 2)
    (z : Coloring α s) (n : Profile s) :
    (∑ a ∈ groupOriginals mu z n, colorMass p s a * p ^ (changes a z).card) ≤
      colorMass p s z *
        (∏ i : Fin s, (3 / (64 : ℝ) ^ (i.val + 1)) ^ (rowCount n i)) *
        (∏ i : Fin s, ((wordCount (rowCount n i) (n i) : ℝ) *
          ∏ h : Color s, colorProb p s h ^ (n i h))) := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.scaleSum, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Profile, OAI.TalagrandThreshold.Selector.groupOriginals, OAI.TalagrandThreshold.colorMass, OAI.TalagrandThreshold.Selector.changes, OAI.TalagrandThreshold.Selector.rowCount, OAI.TalagrandThreshold.wordCount, OAI.TalagrandThreshold.Color, OAI.TalagrandThreshold.colorProb