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 : Finset α), t ∈ 𝒜 → t ⊆ s) (hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ s) :
Finset.card 𝒜 * Finset.card ℬ ≤ 2 ^ Finset.card s * Finset.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 ↑ℬ) :
Finset.card 𝒜 * Finset.card ℬ ≤ 2 ^ Fintype.card α * Finset.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 α * Finset.card (𝒜 ∩ ℬ) ≤ Finset.card 𝒜 * Finset.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 α * Finset.card (𝒜 ∩ ℬ) ≤ Finset.card 𝒜 * Finset.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 ↑ℬ) :
Finset.card 𝒜 * Finset.card ℬ ≤ 2 ^ Fintype.card α * Finset.card (𝒜 ∩ ℬ)

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