mathlib documentation

combinatorics.set_family.harris_kleitman

Harris-Kleitman inequality #

This file proves the Harris-Kleitman inequality. This relates π’œ.card * ℬ.card and 2 ^ card Ξ± * (π’œ ∩ ℬ).card where π’œ and ℬ are upward- or downcard-closed finite families of finsets. This can be interpreted as saying that any two lower sets (resp. any two upper sets) correlate in the uniform measure.

Main declarations #

References #

theorem is_lower_set.non_member_subfamily {Ξ± : Type u_1} [decidable_eq Ξ±] {π’œ : finset (finset Ξ±)} {a : Ξ±} (h : is_lower_set β†‘π’œ) :
theorem is_lower_set.member_subfamily {Ξ± : Type u_1} [decidable_eq Ξ±] {π’œ : finset (finset Ξ±)} {a : Ξ±} (h : is_lower_set β†‘π’œ) :
theorem is_lower_set.member_subfamily_subset_non_member_subfamily {Ξ± : Type u_1} [decidable_eq Ξ±] {π’œ : finset (finset Ξ±)} {a : Ξ±} (h : is_lower_set β†‘π’œ) :
theorem is_lower_set.le_card_inter_finset' {Ξ± : Type u_1} [decidable_eq Ξ±] {π’œ ℬ : finset (finset Ξ±)} {s : finset Ξ±} (hπ’œ : is_lower_set β†‘π’œ) (hℬ : is_lower_set ↑ℬ) (hπ’œs : βˆ€ (t : finset Ξ±), t ∈ π’œ β†’ t βŠ† s) (hℬs : βˆ€ (t : finset Ξ±), t ∈ ℬ β†’ t βŠ† s) :
π’œ.card * ℬ.card ≀ 2 ^ s.card * (π’œ ∩ ℬ).card

Harris-Kleitman inequality: Any two lower sets of finsets correlate.

theorem is_lower_set.le_card_inter_finset {Ξ± : Type u_1} [decidable_eq Ξ±] {π’œ ℬ : finset (finset Ξ±)} [fintype Ξ±] (hπ’œ : is_lower_set β†‘π’œ) (hℬ : is_lower_set ↑ℬ) :
π’œ.card * ℬ.card ≀ 2 ^ fintype.card Ξ± * (π’œ ∩ ℬ).card

Harris-Kleitman inequality: Any two lower sets of finsets correlate.

theorem is_upper_set.card_inter_le_finset {Ξ± : Type u_1} [decidable_eq Ξ±] {π’œ ℬ : finset (finset Ξ±)} [fintype Ξ±] (hπ’œ : is_upper_set β†‘π’œ) (hℬ : is_lower_set ↑ℬ) :
2 ^ fintype.card Ξ± * (π’œ ∩ ℬ).card ≀ π’œ.card * ℬ.card

Harris-Kleitman inequality: Upper sets and lower sets of finsets anticorrelate.

theorem is_lower_set.card_inter_le_finset {Ξ± : Type u_1} [decidable_eq Ξ±] {π’œ ℬ : finset (finset Ξ±)} [fintype Ξ±] (hπ’œ : is_lower_set β†‘π’œ) (hℬ : is_upper_set ↑ℬ) :
2 ^ fintype.card Ξ± * (π’œ ∩ ℬ).card ≀ π’œ.card * ℬ.card

Harris-Kleitman inequality: Lower sets and upper sets of finsets anticorrelate.

theorem is_upper_set.le_card_inter_finset {Ξ± : Type u_1} [decidable_eq Ξ±] {π’œ ℬ : finset (finset Ξ±)} [fintype Ξ±] (hπ’œ : is_upper_set β†‘π’œ) (hℬ : is_upper_set ↑ℬ) :
π’œ.card * ℬ.card ≀ 2 ^ fintype.card Ξ± * (π’œ ∩ ℬ).card

Harris-Kleitman inequality: Any two upper sets of finsets correlate.