# mathlib3documentation

combinatorics.set_family.harris_kleitman

# Harris-Kleitman inequality #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• is_lower_set.le_card_inter_finset: One form of the Harris-Kleitman inequality.

## 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.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 * (𝒜 ℬ).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 ℬ) :
* (𝒜 ℬ).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 ℬ) :
* (𝒜 ℬ).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 * (𝒜 ℬ).card

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