Documentation

Mathlib.Combinatorics.SetFamily.HarrisKleitman

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 IsLowerSet.nonMemberSubfamily {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {a : α} (h : IsLowerSet ↑𝒜) :
theorem IsLowerSet.memberSubfamily {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {a : α} (h : IsLowerSet ↑𝒜) :
theorem IsLowerSet.memberSubfamily_subset_nonMemberSubfamily {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {a : α} (h : IsLowerSet ↑𝒜) :
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.