English
Upper and lower set anticorrelation: the intersection size controls a bound that relates to the product of the cardinalities with powers of 2.
Русский
Антисоотношение верхних и нижних множеств: размер пересечения задаёт границу для произведения кардиналностей с степенями двойки.
LaTeX
$$$$2^{|X|}\\;|\\mathcal{A}\\cap\\mathcal{B}| \\le |\\mathcal{A}|\\cdot|\\mathcal{B}|$$$$
Lean4
/-- **Harris-Kleitman inequality**: Upper sets and lower sets of finsets anticorrelate. -/
theorem card_inter_le_finset (h𝒜 : IsUpperSet (𝒜 : Set (Finset α))) (hℬ : IsLowerSet (ℬ : Set (Finset α))) :
2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ :=
by
rw [← isLowerSet_compl, ← coe_compl] at h𝒜
have := h𝒜.le_card_inter_finset hℬ
rwa [card_compl, Fintype.card_finset, tsub_mul, tsub_le_iff_tsub_le, ← mul_tsub, ←
card_sdiff_of_subset inter_subset_right, sdiff_inter_self_right, sdiff_compl, _root_.inf_comm] at this
