infSum — Mathlib

English

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

Русский

InfSum семейства множеств 𝒜 — сумма по всем s из размера truncatedInf(𝒜, s), деленная на (|s| умноженное на C(|α|, |s|)).

LaTeX

$$$\mathrm{infSum}(\mathcal{A}) = \displaystyle \sum_{s} \frac{\#(\mathrm{truncatedInf}(\mathcal{A}, s))}{\left(|s| \cdot {\binom{\lvert \alpha \rvert}{|s|}}\right)}$$$

Lean4

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

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