Independent sets of set mappings on pairs

DefinitionIndependent set of a set mapping on pairs#✓fully proved

Let \(n\) be a natural number and let \(f\) assign to each unordered pair \(\{x, y\}\) of elements of \(\{0, \dots, n-1\}\) (possibly with \(x = y\)) an element of \(\{0, \dots, n-1\}\). A finite set \(X \subseteq \{0, \dots, n-1\}\) is independent for \(f\) if \(f(\{x, y\}) \notin X\) for all distinct \(x, y \in X\).

def IsIndependentFor {n : ℕ} (f : Sym2 (Fin n) → Fin n) (X : Finset (Fin n)) : Prop :=
  ∀ x ∈ X, ∀ y ∈ X, x ≠ y → f s(x, y) ∉ X

Used by 1

Used byIndependence number of set mappings on pairs

DefinitionIndependence number of set mappings on pairs#✓fully proved

For a natural number \(n\), \(g(n)\) is the largest \(k\) such that every map \(f\) from the unordered pairs \(\{x, y\}\) of elements of \(\{0, \dots, n-1\}\) (possibly with \(x = y\)) to \(\{0, \dots, n-1\}\) with \(f(\{x, y\}) \notin \{x, y\}\) for all distinct \(x, y\) has an independent set of at least \(k\) elements, that is, a set \(X \subseteq \{0, \dots, n-1\}\) with \(|X| \ge k\) and \(f(\{x, y\}) \notin X\) for all distinct \(x, y \in X\). If no largest such \(k\) exists, \(g(n) = 0\); this happens for \(n = 2\), where no such \(f\) exists.

noncomputable def setMappingIndependence (n : ℕ) : ℕ :=
  sSup {k | ∀ f : Sym2 (Fin n) → Fin n, (∀ x y, x ≠ y → f s(x, y) ≠ x ∧ f s(x, y) ≠ y) →
    ∃ X : Finset (Fin n), IsIndependentFor f X ∧ k ≤ X.card}

Uses 1 · Used by 1

Statement usesIndependent set of a set mapping on pairs

Used byStatement of Erdős Problem 1025

DefinitionStatement of Erdős Problem 1025#✓fully proved

For a natural number \(n\), let \(g(n)\) be the largest \(k\) such that every map \(f\) from the unordered pairs of elements of \(\{0, \dots, n-1\}\) to \(\{0, \dots, n-1\}\) with \(f(\{x, y\}) \notin \{x, y\}\) for all distinct \(x, y\) admits a set \(X\) of at least \(k\) elements with \(f(\{x, y\}) \notin X\) for all distinct \(x, y \in X\) (and \(g(n) = 0\) if no largest such \(k\) exists). This is the proposition that \(g(n) \asymp \sqrt{n}\) as \(n \to \infty\), that is, that there are constants \(c, C > 0\) with \(c \sqrt{n} \le g(n) \le C \sqrt{n}\) for all sufficiently large \(n\).

Spencer proved the lower bound and Conlon, Fox and Sudakov the upper bound.

def setMappingIndependenceAsymp : Prop :=
  Asymptotics.IsTheta Filter.atTop (fun n : ℕ => (setMappingIndependence n : ℝ))
    (fun n : ℕ => Real.sqrt n)

Uses 1 · Used by 1

Statement usesIndependence number of set mappings on pairs

Used byErdős Problem 1025 (Spencer; Conlon, Fox and Sudakov)

TheoremErdős Problem 1025 (Spencer; Conlon, Fox and Sudakov)#●ready to prove

For a natural number \(n\), let \(g(n)\) be the largest \(k\) such that every map \(f\) from the unordered pairs of elements of \(\{0, \dots, n-1\}\) to \(\{0, \dots, n-1\}\) with \(f(\{x, y\}) \notin \{x, y\}\) for all distinct \(x, y\) admits a set \(X\) of at least \(k\) elements with \(f(\{x, y\}) \notin X\) for all distinct \(x, y \in X\) (and \(g(n) = 0\) if no largest such \(k\) exists). Then there are constants \(c, C > 0\) such that \(c \sqrt{n} \le g(n) \le C \sqrt{n}\) for all sufficiently large \(n\), that is, \(g(n) \asymp \sqrt{n}\) as \(n \to \infty\).

public theorem_wanted setMappingIndependenceAsymp_holds : setMappingIndependenceAsymp

Sources

• T. F. Bloom, Erdős Problems, Problem #1025, https://www.erdosproblems.com/1025 (status SOLVED (LEAN)); resolution: J. Spencer, Turán's theorem for k-graphs, Discrete Math. (1972), 183-186; D. Conlon, J. Fox and B. Sudakov, Short proofs of some extremal results II, J. Combin. Theory Ser. B (2016), 173-196, Spencer: g(n) ≫ n^{1/2}; Conlon-Fox-Sudakov: g(n) ≪ n^{1/2} (erdosproblems.com/1025), https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1025.lean#L829.

Uses 1

Statement usesStatement of Erdős Problem 1025

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.