supSum — Mathlib

English

The supSum of a set family 𝒜 is the sum over all ground sets s of the size of truncatedSup 𝒜 s, divided by ((card α - #s) times choose(card α, #s)).

Русский

SupSum семейства 𝒜 — сумма по всем s размера truncatedSup(𝒜, s), деленная на ((|α|−|s|)·{|α| choose |s|}).

LaTeX

$$$\mathrm{supSum}(\mathcal{A}) = \displaystyle \sum_{s} \frac{\#(\mathrm{truncatedSup}(\mathcal{A}, s))}{\bigl((|\alpha| - |s|) \cdot {\binom{|\alpha|}{|s|}}\bigr)}$$$

Lean4

/-- Weighted sum of the size of the truncated suprema of a set family. Relevant to the
Ahlswede-Zhang identity. -/
def supSum (𝒜 : Finset (Finset α)) : ℚ :=
  ∑ s, #(truncatedSup 𝒜 s) / ((card α - #s) * (card α).choose #s)

Похожие утверждения