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 ↑𝒜)
:
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 ↑𝒜)
:
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.