SelectorGlobalCostProfiles.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Summing the full-profile weights

The reconstruction sets may depend on the entire profile. Once their counting bound has been replaced by the uniform entropy bound, the remaining full profiles can be grouped by row counts. The literal word-count weights have total mass at most one within each such group.

theorem OAI.TalagrandThreshold.Selector.sum_profile_weights_lt_one_twentieth line 23
Source documentation
The full-profile sum satisfies the selector budget for any finite family whose row-count vectors are nonzero. No independence of the rows of the profile family is required.
```
theorem sum_profile_weights_lt_one_twentieth (p : ℝ) (s : ℕ) (hp : 0 < p)
    (hs : p * scaleSum s ≤ 1 / 2) (N : Finset (Profile s))
    (hN : ∀ n ∈ N, rowCount n ≠ 0) :
    (∑ n ∈ N,
      (∏ 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)))) < 1 / 20 := by
…
```
Mentions: OAI.TalagrandThreshold.scaleSum, OAI.TalagrandThreshold.Selector.Profile, OAI.TalagrandThreshold.Selector.rowCount, OAI.TalagrandThreshold.wordCount, OAI.TalagrandThreshold.Color, OAI.TalagrandThreshold.colorProb