English
For a finite α and a finite family 𝒜 of subsets of α, the sum infSum of the complement family 𝒜ᶜˢ plus the sum supSum of 𝒜 equals |α| times the sum over k in range(|α|) of k^{-1} plus 1.
Русский
Для конечного α и конечного семейства 𝒜 подмножеств α сумма infSum дополнений 𝒜ᶜˢ плюс сумма supSum 𝒜 равны |α| · ∑_{k∈range(|α|)} k^{-1} + 1.
LaTeX
$$$\infSum 𝒜^{cS} + \supSum 𝒜 = \lvert \alpha \rvert \sum_{k \in \mathrm{range}(\lvert \alpha \rvert)} k^{-1} + 1$$$
Lean4
/-- The **Ahlswede-Zhang Identity**. -/
theorem infSum_compls_add_supSum (𝒜 : Finset (Finset α)) :
infSum 𝒜ᶜˢ + supSum 𝒜 = card α * ∑ k ∈ range (card α), (k : ℚ)⁻¹ + 1 :=
by
unfold infSum supSum
rw [← @map_univ_of_surjective (Finset α) _ _ _ ⟨compl, compl_injective⟩ compl_surjective, sum_map]
simp only [Function.Embedding.coeFn_mk, univ_map_embedding, ← compl_truncatedSup, ← sum_add_distrib, card_compl,
cast_sub (card_le_univ _), choose_symm (card_le_univ _), ← add_div, sub_add_cancel,
Fintype.sum_div_mul_card_choose_card]
