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

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

References

• [D. J. Kleitman, Families of non-disjoint subsets][kleitman1966]

theorem IsLowerSet.nonMemberSubfamily {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {a : α} (h : IsLowerSet ↑𝒜) : IsLowerSet ↑(Finset.nonMemberSubfamily a 𝒜)

theorem IsLowerSet.memberSubfamily {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {a : α} (h : IsLowerSet ↑𝒜) : IsLowerSet ↑(Finset.memberSubfamily a 𝒜)

theorem IsLowerSet.memberSubfamily_subset_nonMemberSubfamily {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {a : α} (h : IsLowerSet ↑𝒜) : Finset.memberSubfamily a 𝒜 ⊆ Finset.nonMemberSubfamily a 𝒜

theorem IsLowerSet.le_card_inter_finset' {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {ℬ : Finset (Finset α)} {s : Finset α} (h𝒜 : IsLowerSet ↑𝒜) (hℬ : IsLowerSet ↑ℬ) (h𝒜s : ∀ t ∈ 𝒜, t ⊆ s) (hℬs : ∀ t ∈ ℬ, t ⊆ s) : 𝒜.card * ℬ.card ≤ 2 ^ s.card * (𝒜 ∩ ℬ).card

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

theorem IsLowerSet.le_card_inter_finset {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {ℬ : Finset (Finset α)} [Fintype α] (h𝒜 : IsLowerSet ↑𝒜) (hℬ : IsLowerSet ↑ℬ) : 𝒜.card * ℬ.card ≤ 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card

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

theorem IsUpperSet.card_inter_le_finset {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {ℬ : Finset (Finset α)} [Fintype α] (h𝒜 : IsUpperSet ↑𝒜) (hℬ : IsLowerSet ↑ℬ) : 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card ≤ 𝒜.card * ℬ.card

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

theorem IsLowerSet.card_inter_le_finset {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {ℬ : Finset (Finset α)} [Fintype α] (h𝒜 : IsLowerSet ↑𝒜) (hℬ : IsUpperSet ↑ℬ) : 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card ≤ 𝒜.card * ℬ.card

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

theorem IsUpperSet.le_card_inter_finset {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {ℬ : Finset (Finset α)} [Fintype α] (h𝒜 : IsUpperSet ↑𝒜) (hℬ : IsUpperSet ↑ℬ) : 𝒜.card * ℬ.card ≤ 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card

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