Turán systems

DefinitionTurán system#✓fully proved

Let \(n\), \(s\), \(r\) be natural numbers. A family \(H\) of subsets of \(\{0, 1, \dots, n-1\}\) is a Turán \((n, s, r)\)-system when \(0 < r < s \le n\), \(H\) is \(r\)-uniform (every member of \(H\) has exactly \(r\) elements), and every \(s\)-element subset of \(\{0, 1, \dots, n-1\}\) contains some member of \(H\).

public def IsTuranSystem (n s r : ℕ) (H : Finset (Finset (Fin n))) : Prop :=
  0 < r ∧ r < s ∧ s ≤ n ∧ SetFamily.IsUniform H r ∧
    ∀ T ∈ Finset.powersetCard s (Finset.univ : Finset (Fin n)), ∃ e ∈ H, e ⊆ T

Uses 1 · Used by 12

Statement usesUniform hypergraphs

Used byThe complete \(r\)-graph is a Turán system · Turán systems cover every \(s\)-set · Turán systems exist · A Turán system has \(s \le n\) · A Turán system has \(r < s\) · Membership in the realized sizes · Turán systems have positive uniformity · Realized sizes of Turán systems · Some size of a Turán system is realized · The Turán number is attained · Turán systems are at least as large as the Turán number · Turán systems are uniform

TheoremTurán systems have positive uniformity#✓fully proved

Let \(n\), \(s\), \(r\) be natural numbers and let \(H\) be a Turán system with parameters \(n\), \(s\), \(r\), whose definition includes \(0 < r < s \le n\). Then \(0 < r\).

public theorem pos_of_isTuran (n s r : ℕ) (H : Finset (Finset (Fin n)))
    (h : IsTuranSystem n s r H) : 0 < r

Uses 2

Statement usesTurán system

Proof usesUniform hypergraphs

TheoremA Turán system has \(r < s\)#✓fully proved

Let \(n\), \(s\), \(r\) be natural numbers and let \(H\) be a Turán \((n, s, r)\)-system. Then \(r < s\).

public theorem lt_of_isTuran (n s r : ℕ) (H : Finset (Finset (Fin n)))
    (h : IsTuranSystem n s r H) : r < s

Uses 2

Statement usesTurán system

Proof usesUniform hypergraphs

TheoremA Turán system has \(s \le n\)#✓fully proved

Let \(n\), \(s\), \(r\) be natural numbers and let \(H\) be a Turán \((n, s, r)\)-system. Then \(s \le n\).

public theorem le_of_isTuran (n s r : ℕ) (H : Finset (Finset (Fin n)))
    (h : IsTuranSystem n s r H) : s ≤ n

Uses 2

Statement usesTurán system

Proof usesUniform hypergraphs

TheoremTurán systems are uniform#✓fully proved

Let \(n\), \(s\), \(r\) be natural numbers. If \(H\) is a Turán system with parameters \(n\), \(s\), \(r\), then \(H\) is \(r\)-uniform: every member of \(H\) has exactly \(r\) elements.

public theorem uniform_of_isTuran (n s r : ℕ) (H : Finset (Finset (Fin n)))
    (h : IsTuranSystem n s r H) : SetFamily.IsUniform H r

Uses 2

Statement usesUniform hypergraphs · Turán system

TheoremTurán systems cover every \(s\)-set#✓fully proved

Let \(n\), \(s\), \(r\) be natural numbers and let \(H\) be a Turán \((n, s, r)\)-system. Then every \(s\)-element subset \(T\) of \(\{0, 1, \dots, n-1\}\) contains some member \(e\) of \(H\).

public theorem cover_of_isTuran (n s r : ℕ) (H : Finset (Finset (Fin n)))
    (h : IsTuranSystem n s r H) :
    ∀ T ∈ Finset.powersetCard s (Finset.univ : Finset (Fin n)),
      ∃ e ∈ H, e ⊆ T

Uses 2

Statement usesTurán system

Proof usesUniform hypergraphs

DefinitionThe complete \(r\)-graph#✓fully proved

For natural numbers \(n\) and \(r\), the complete \(r\)-graph on \(n\) vertices is the family of all \(r\)-element subsets of \(\{0, 1, \dots, n-1\}\).

public def completeGraph (n r : ℕ) : Finset (Finset (Fin n)) :=
  Finset.powersetCard r (Finset.univ : Finset (Fin n))

Used by 4

Used byThe complete \(r\)-graph is a Turán system · The complete \(r\)-graph is \(r\)-uniform · Turán systems exist · Some size of a Turán system is realized

TheoremThe complete \(r\)-graph is \(r\)-uniform#✓fully proved

For all natural numbers \(n\) and \(r\), every member of the complete \(r\)-graph on \(\{0, 1, \dots, n-1\}\) has exactly \(r\) elements.

public theorem completeGraph_uniform (n r : ℕ) :
    SetFamily.IsUniform (completeGraph n r) r

Uses 2 · Used by 1

Statement usesUniform hypergraphs · The complete \(r\)-graph

Used byThe complete \(r\)-graph is a Turán system

TheoremThe complete \(r\)-graph is a Turán system#✓fully proved

Let \(n\), \(s\), \(r\) be natural numbers with \(0 < r < s \le n\). Then the complete \(r\)-graph on \(\{0, 1, \dots, n-1\}\) (the family of all its \(r\)-element subsets) is a Turán \((n, s, r)\)-system.

public theorem completeGraph_isTuran (n s r : ℕ)
    (hd : 0 < r ∧ r < s ∧ s ≤ n) :
    IsTuranSystem n s r (completeGraph n r)

Uses 4 · Used by 2

Statement usesTurán system · The complete \(r\)-graph

Proof usesUniform hypergraphs · The complete \(r\)-graph is \(r\)-uniform

Used byTurán systems exist · Some size of a Turán system is realized

DefinitionRealized sizes of Turán systems#✓fully proved

For natural numbers \(n\), \(s\), \(r\), the set of realized sizes is the set of natural numbers \(k\) such that some Turán system with parameters \(n\), \(s\), \(r\) on the vertex set \(\{0, \dots, n-1\}\) has exactly \(k\) members.

public def realizedCounts (n s r : ℕ) : Set ℕ :=
  { k | ∃ H, IsTuranSystem n s r H ∧ H.card = k }

Uses 1 · Used by 7

Statement usesTurán system

Used byLower bounds on the Turán number · Membership in the realized sizes · Some size of a Turán system is realized · Turán number · The Turán number is attained · Turán systems are at least as large as the Turán number · The Turán number is a realized size

TheoremMembership in the realized sizes#✓fully proved

For natural numbers \(n\), \(s\), \(r\), \(k\), the number \(k\) lies in the set of realized sizes for \((n, s, r)\) if and only if some Turán \((n, s, r)\)-system \(H\) has exactly \(k\) members.

public theorem mem_realizedCounts (n s r k : ℕ) :
    k ∈ realizedCounts n s r ↔ ∃ H, IsTuranSystem n s r H ∧ H.card = k

Uses 2

Statement usesTurán system · Realized sizes of Turán systems

TheoremTurán systems exist#✓fully proved

For all natural numbers \(n\), \(s\), \(r\) with \(0 < r < s \le n\), there is a Turán \((n, s, r)\)-system.

public theorem exists_system (n s r : ℕ) (hd : 0 < r ∧ r < s ∧ s ≤ n) :
    ∃ H, IsTuranSystem n s r H

Uses 3

Statement usesTurán system

Proof usesThe complete \(r\)-graph · The complete \(r\)-graph is a Turán system

TheoremSome size of a Turán system is realized#✓fully proved

For natural numbers \(n\), \(s\), \(r\) with \(0 < r < s \le n\), the set of realized sizes for \(n\), \(s\), \(r\) is nonempty: some natural number \(k\) is the number of members of a Turán system with parameters \(n\), \(s\), \(r\).

public theorem realizedCounts_nonempty (n s r : ℕ)
    (hd : 0 < r ∧ r < s ∧ s ≤ n) : ∃ k, k ∈ realizedCounts n s r

Uses 4 · Used by 1

Statement usesRealized sizes of Turán systems

Proof usesTurán system · The complete \(r\)-graph · The complete \(r\)-graph is a Turán system

Used byThe Turán number is a realized size

DefinitionTurán number#✓fully proved

For natural numbers \(n\), \(s\), \(r\), the Turán number \(T(n, s, r)\) is the least element of the set of realized sizes for \(n\), \(s\), \(r\), that is, the least number of members of a Turán system with parameters \(n\), \(s\), \(r\), and \(T(n, s, r) = 0\) if no such system exists.

public noncomputable def turanNumber (n s r : ℕ) : ℕ := by
  classical
  exact if h : ∃ k, k ∈ realizedCounts n s r then Nat.find h else 0

Uses 1 · Used by 4

Statement usesRealized sizes of Turán systems

Used byLower bounds on the Turán number · The Turán number is attained · Turán systems are at least as large as the Turán number · The Turán number is a realized size

TheoremThe Turán number is a realized size#✓fully proved

Let \(n\), \(s\), \(r\) be natural numbers with \(0 < r < s \le n\) and let \(T(n, s, r)\) denote the Turán number. Then \(T(n, s, r)\) belongs to the set of realized sizes for \(n\), \(s\), \(r\).

public theorem turanNumber_mem (n s r : ℕ) (hd : 0 < r ∧ r < s ∧ s ≤ n) :
    turanNumber n s r ∈ realizedCounts n s r

Uses 3 · Used by 2

Statement usesRealized sizes of Turán systems · Turán number

Proof usesSome size of a Turán system is realized

Used byLower bounds on the Turán number · The Turán number is attained

TheoremThe Turán number is attained#✓fully proved

Let \(n\), \(s\), \(r\) be natural numbers with \(0 < r < s \le n\) and let \(T(n, s, r)\) denote the Turán number. Then some Turán system with parameters \(n\), \(s\), \(r\) has exactly \(T(n, s, r)\) members.

public theorem turanNumber_attains (n s r : ℕ)
    (hd : 0 < r ∧ r < s ∧ s ≤ n) :
    ∃ H, IsTuranSystem n s r H ∧ H.card = turanNumber n s r

Uses 4

Statement usesTurán system · Turán number

Proof usesRealized sizes of Turán systems · The Turán number is a realized size

TheoremTurán systems are at least as large as the Turán number#✓fully proved

Let \(n\), \(s\), \(r\) be natural numbers and let \(T(n, s, r)\) denote the Turán number. If \(H\) is a Turán system with parameters \(n\), \(s\), \(r\), then \(T(n, s, r) \le |H|\).

public theorem turanNumber_le (n s r : ℕ) (H : Finset (Finset (Fin n)))
    (hH : IsTuranSystem n s r H) : turanNumber n s r ≤ H.card

Uses 3

Statement usesTurán system · Turán number

Proof usesRealized sizes of Turán systems

TheoremLower bounds on the Turán number#✓fully proved

Let \(n\), \(s\), \(r\), \(b\) be natural numbers with \(0 < r < s \le n\). If \(b \le k\) for every \(k\) in the set of realized sizes for \((n, s, r)\) (the sizes of Turán \((n, s, r)\)-systems), then \(b\) is at most the Turán number \(T(n, s, r)\).

public theorem le_turanNumber (n s r b : ℕ)
    (hb : ∀ k ∈ realizedCounts n s r, b ≤ k)
    (hd : 0 < r ∧ r < s ∧ s ≤ n) : b ≤ turanNumber n s r

Uses 3

Statement usesRealized sizes of Turán systems · Turán number

Proof usesThe Turán number is a realized size

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.