English
Let α be a finite nonempty type and s ⊊ α with s ≠ univ. Then the supremum sum of the singleton {s} equals |α| times the sum of k^{-1} for k in 0,...,|α|-1 (interpreted in ℚ).
Русский
Пусть α — конечное непустое множество, и выбрано подмножество s ⊂ α, неполное (s ≠ univ). Тогда supSum({s}) равно |α| · ∑_{k=0}^{|α|-1} k^{-1} (в ℚ).
LaTeX
$$$\operatornamename{supSum}({s}) = |\alpha| \sum_{k \in \mathrm{range}(|\alpha|)} k^{-1}$$$
Lean4
@[simp]
theorem supSum_singleton (hs : s ≠ univ) :
supSum ({ s } : Finset (Finset α)) = card α * ∑ k ∈ range (card α), (k : ℚ)⁻¹ :=
by
have :
∀ t : Finset α,
(card α - #(truncatedSup { s } t) : ℚ) / ((card α - #t) * (card α).choose #t) =
if t ⊆ s then (card α - #s : ℚ) / ((card α - #t) * (card α).choose #t) else 0 :=
by
rintro t
simp_rw [truncatedSup_singleton, le_iff_subset]
split_ifs <;> simp
simp_rw [← sub_eq_of_eq_add (Fintype.sum_div_mul_card_choose_card α), eq_sub_iff_add_eq, ← eq_sub_iff_add_eq', supSum,
← sum_sub_distrib, ← sub_div]
rw [sum_congr rfl fun t _ ↦ this t, sum_ite, sum_const_zero, add_zero, filter_subset_univ, sum_powerset, ←
binomial_sum_eq ((card_lt_iff_ne_univ _).2 hs), eq_comm]
refine sum_congr rfl fun n _ ↦ ?_
rw [mul_div_assoc, ← nsmul_eq_mul]
exact sum_powersetCard n s fun m ↦ (card α - #s : ℚ) / ((card α - m) * (card α).choose m)
