English
Holley’s inequality specialized to Finset families: under monotone μ and equal total weight of f and g, the weighted sums satisfy a majorization-type inequality.
Русский
Неравенство Холли для семейств финсет: при монотонной μ и равном суммарном весе f и g, взвешанные суммы удовлетворяют подобному мажорированию неравенству.
LaTeX
$$$$\\sum_{a} μ(a) f(a) \\le \\sum_{a} μ(a) g(a)$$$$
Lean4
/-- **Harris-Kleitman inequality**: Any two upper sets of finsets correlate. -/
theorem le_card_inter_finset (h𝒜 : IsUpperSet (𝒜 : Set (Finset α))) (hℬ : IsUpperSet (ℬ : Set (Finset α))) :
#𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ) :=
by
rw [← isLowerSet_compl, ← coe_compl] at h𝒜
have := h𝒜.card_inter_le_finset hℬ
rwa [card_compl, Fintype.card_finset, tsub_mul, le_tsub_iff_le_tsub, ← mul_tsub, ←
card_sdiff_of_subset inter_subset_right, sdiff_inter_self_right, sdiff_compl, _root_.inf_comm] at this
· exact mul_le_mul_left' (card_le_card inter_subset_right) _
· rw [← Fintype.card_finset]
exact mul_le_mul_right' (card_le_univ _) _
