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