SelectorCountingWordsProducts.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Products of counting-word weights

An arbitrary finite collection of row profiles has total counting-word weight at most one when the nonnegative color weights have total mass at most one. The coefficients are the actual cardinalities of words with each profile.

theorem OAI.TalagrandThreshold.sum_prod_le_prod_sum_of_support line 20

theorem OAI.TalagrandThreshold.sum_prod_wordCount_weight_le_one line 48

Source documentation

Summing the literal counting-word weights over any finite set of row profiles is bounded by one. Neither the row type nor the color type needs to be nonempty.

theorem sum_prod_wordCount_weight_le_one {I H : Type*} [Fintype I]
    [Fintype H] [DecidableEq H] (t : I → ℕ) (E : Finset (I → H → ℕ))
    (π : H → ℝ) (hπ : ∀ h, 0 ≤ π h) (hπsum : (∑ h, π h) ≤ 1) :
    (∑ n ∈ E, ∏ i, ((wordCount (t i) (n i) : ℝ) * ∏ h, π h ^ (n i h))) ≤ 1 := by
…

Mentions: OAI.TalagrandThreshold.wordCount