Set families

TheoremFour functions theorem#

The Four Functions Theorem, aka Ahlswede-Daykin Inequality.

four_functions_theorem.{u_1, u_2} {α : Type u_1} {β : Type u_2} [DistribLattice α] [CommSemiring β]
  [LinearOrder β] [IsStrictOrderedRing β] [ExistsAddOfLE β] (f₁ f₂ f₃ f₄ : α → β) [DecidableEq α]
  (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄)
  (h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)) (s t : Finset α) :
  (∑ a ∈ s, f₁ a) * ∑ a ∈ t, f₂ a ≤ (∑ a ∈ s ⊼ t, f₃ a) * ∑ a ∈ s ⊻ t, f₄ a

Sources

• Mathlib documentation: four_functions_theorem
• Source of four_functions_theorem in Mathlib/Combinatorics/SetFamily/FourFunctions.lean
• Mathlib overview: Combinatorics › Set families
• 1000+ theorems list: Q4695203
• 1000+ theorems project: Q4695203
• Wikipedia: Four functions theorem
• Wikidata: Q4695203

Mathlibfour_functions_theorem

Uses 3

Statement usesFinite set · Natural number

Proof usesOrdered ring

TheoremHarris-Kleitman inequality#

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

IsLowerSet.le_card_inter_finset.{u_1} {α : Type u_1} [DecidableEq α] {𝒜 ℬ : Finset (Finset α)}
  [Fintype α] (h𝒜 : IsLowerSet ↑𝒜) (hℬ : IsLowerSet ↑ℬ) :
  𝒜.card * ℬ.card ≤ 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card

Sources

• Mathlib documentation: IsLowerSet.le_card_inter_finset
• Source of IsLowerSet.le_card_inter_finset in Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean
• Mathlib overview: Combinatorics › Set families

MathlibIsLowerSet.le_card_inter_finset

Uses 3 · Used by 1

Statement usesFinite set · Natural number

Proof usesOrdered ring

Used byKleitman's theorem

TheoremAhlswede-Zhang identity#

The Ahlswede-Zhang Identity.

AhlswedeZhang.infSum_eq_one.{u_1} {α : Type u_1} [Fintype α] [DecidableEq α] {𝒜 : Finset (Finset α)}
  [Nonempty α] (h𝒜₁ : 𝒜.Nonempty) (h𝒜₀ : ∅ ∉ 𝒜) : AhlswedeZhang.infSum 𝒜 = 1

Sources

• Mathlib documentation: AhlswedeZhang.infSum_eq_one
• Source of AhlswedeZhang.infSum_eq_one in Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
• Mathlib overview: Combinatorics › Set families

MathlibAhlswedeZhang.infSum_eq_one

Uses 5

Statement usesFinite set · Rational number

Proof usesCharacteristic zero · Field \(\Q\) of rational numbers · Formula for the Number of Combinations

TheoremLYM inequality#

The Lubell-Yamamoto-Meshalkin inequality, also known as the LYM inequality.

If 𝒜 is an antichain, then the sum of the proportion of elements it takes from each layer is less than 1.

Finset.lubell_yamamoto_meshalkin_inequality_sum_card_div_choose.{u_1, u_2} {𝕜 : Type u_1}
  {α : Type u_2} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Fintype α]
  {𝒜 : Finset (Finset α)} (h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜) :
  ∑ r ∈ Finset.range (Fintype.card α + 1), ↑(𝒜.slice r).card / ↑((Fintype.card α).choose r) ≤ 1

Sources

• Mathlib documentation: Finset.lubell_yamamoto_meshalkin_inequality_sum_card_div_choose
• Source of Finset.lubell_yamamoto_meshalkin_inequality_sum_card_div_choose in Mathlib/Combinatorics/SetFamily/LYM.lean
• Mathlib overview: Combinatorics › Set families

MathlibFinset.lubell_yamamoto_meshalkin_inequality_sum_card_div_choose

Uses 5 · Used by 1

Statement usesFinite set · Rational number

Proof usesCharacteristic zero · Formula for the Number of Combinations · Ordered ring

Used bySperner's theorem

TheoremSperner's theorem#

Sperner's theorem. The size of an antichain in Finset α is bounded by the size of the maximal layer in Finset α. This precisely means that Finset α is a Sperner order.

IsAntichain.sperner.{u_2} {α : Type u_2} [Fintype α] {𝒜 : Finset (Finset α)}
  (h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜) :
  𝒜.card ≤ (Fintype.card α).choose (Fintype.card α / 2)

Sources

• Mathlib documentation: IsAntichain.sperner
• Source of IsAntichain.sperner in Mathlib/Combinatorics/SetFamily/LYM.lean
• Mathlib overview: Combinatorics › Set families
• 1000+ theorems list: Q2226786
• 1000+ theorems project: Q2226786
• Wikipedia: Sperner's theorem
• Wikidata: Q2226786

MathlibIsAntichain.sperner

Uses 3

Statement usesFinite set · Natural number

Proof usesLYM inequality

TheoremMaximum size of an intersecting family#

Mathlib states this as Set.Intersecting.is_max_iff_card_eq.

Set.Intersecting.is_max_iff_card_eq.{u_1} {α : Type u_1} [BooleanAlgebra α] [Nontrivial α]
  [Fintype α] {s : Finset α} (hs : (↑s).Intersecting) :
  (∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t) ↔ 2 * s.card = Fintype.card α

Sources

• Mathlib documentation: Set.Intersecting.is_max_iff_card_eq
• Source of Set.Intersecting.is_max_iff_card_eq in Mathlib/Combinatorics/SetFamily/Intersecting.lean
• Mathlib overview: Combinatorics › Set families

MathlibSet.Intersecting.is_max_iff_card_eq

Uses 2 · Used by 1

Statement usesFinite set · Natural number

Used byKleitman's theorem

TheoremKleitman's theorem#

Kleitman's theorem. An intersecting family on n elements contains at most 2ⁿ⁻¹ sets, and each further intersecting family takes at most half of the sets that are in no previous family.

Finset.card_biUnion_le_of_intersecting.{u_1, u_2} {ι : Type u_1} {α : Type u_2} [Fintype α]
  [DecidableEq α] [Nonempty α] (s : Finset ι) (f : ι → Finset (Finset α))
  (hf : ∀ i ∈ s, (↑(f i)).Intersecting) :
  (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)

Sources

• Mathlib documentation: Finset.card_biUnion_le_of_intersecting
• Source of Finset.card_biUnion_le_of_intersecting in Mathlib/Combinatorics/SetFamily/Kleitman.lean
• Mathlib overview: Combinatorics › Set families

MathlibFinset.card_biUnion_le_of_intersecting

Uses 5

Statement usesFinite set · Natural number

Proof usesHarris-Kleitman inequality · Maximum size of an intersecting family · The Number of Subsets of a Set

DefinitionVC dimension#

The Vapnik-Chervonenkis dimension of a set family is the maximal size of a set it shatters.

Finset.vcDim.{u_1} {α : Type u_1} [DecidableEq α] (𝒜 : Finset (Finset α)) : ℕ

Sources

• Mathlib documentation: Finset.vcDim
• Source of Finset.vcDim in Mathlib/Combinatorics/SetFamily/Shatter.lean
• Mathlib overview: Combinatorics › Set families

MathlibFinset.vcDim

Uses 2 · Used by 1

Statement usesFinite set · Natural number

Used bySauer-Shelah lemma

TheoremSauer-Shelah lemma#

The Sauer-Shelah lemma.

Finset.card_shatterer_le_sum_vcDim.{u_1} {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)}
  [Fintype α] : 𝒜.shatterer.card ≤ ∑ k ≤ 𝒜.vcDim, (Fintype.card α).choose k

Sources

• Mathlib documentation: Finset.card_shatterer_le_sum_vcDim
• Source of Finset.card_shatterer_le_sum_vcDim in Mathlib/Combinatorics/SetFamily/Shatter.lean
• Mathlib overview: Combinatorics › Set families

MathlibFinset.card_shatterer_le_sum_vcDim

Uses 2

Statement usesVC dimension

Proof usesFormula for the Number of Combinations

TheoremKruskal-Katona theorem#

The Kruskal-Katona theorem.

Given a set family 𝒜 consisting of r-sets, and 𝒞 an initial segment of the colex order of the same size, the shadow of 𝒞 is smaller than the shadow of 𝒜. In particular, this gives that the minimum shadow size is achieved by initial segments of colex.

Finset.kruskal_katona {n r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))} (h𝒜r : Set.Sized r ↑𝒜)
  (h𝒞𝒜 : 𝒞.card ≤ 𝒜.card) (h𝒞 : Finset.Colex.IsInitSeg 𝒞 r) : 𝒞.shadow.card ≤ 𝒜.shadow.card

Sources

• Mathlib documentation: Finset.kruskal_katona
• Source of Finset.kruskal_katona in Mathlib/Combinatorics/SetFamily/KruskalKatona.lean
• Mathlib overview: Combinatorics › Set families
• 1000+ theorems list: Q3527102
• 1000+ theorems project: Q3527102
• Wikipedia: Kruskal–Katona theorem
• Wikidata: Q3527102

MathlibFinset.kruskal_katona

Uses 2 · Used by 1

Statement usesFinite set · Natural number

Used byErdős–Ko–Rado theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.