mathlib3 documentation

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 #

References #

source
theorem is_lower_set.non_member_subfamily {α : Type u_1} [decidable_eq α] {𝒜 : finset (finset α)} {a : α} (h : is_lower_set ↑𝒜) :
is_lower_set ↑(finset.non_member_subfamily a 𝒜)
source
theorem is_lower_set.member_subfamily {α : Type u_1} [decidable_eq α] {𝒜 : finset (finset α)} {a : α} (h : is_lower_set ↑𝒜) :
is_lower_set ↑(finset.member_subfamily a 𝒜)
source
theorem is_lower_set.member_subfamily_subset_non_member_subfamily {α : Type u_1} [decidable_eq α] {𝒜 : finset (finset α)} {a : α} (h : is_lower_set ↑𝒜) :
finset.member_subfamily a 𝒜 ⊆ finset.non_member_subfamily a 𝒜
source
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.

source
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.

source
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.

source
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.

source
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.