Shamir's problem

DefinitionProbability of a perfect matching in a random \(3\)-uniform hypergraph#✓fully proved

For natural numbers \(n\) and \(\ell\), let \(T\) be the set of \(3\)-element subsets of \(\{0, 1, \dots, 3n - 1\}\). This is the proportion of the \(\ell\)-element subsets \(E \subseteq T\) that contain \(n\) pairwise disjoint triples, that is, the probability that the uniformly random \(3\)-uniform hypergraph on \(3n\) vertices with \(\ell\) edges has a perfect matching. When \(\ell > \binom{3n}{3}\) there is no such hypergraph and the value is \(0\).

noncomputable def matchingProbability (n ℓ : ℕ) : ℝ :=
  (((Finset.univ.filter fun e : Finset (Fin (3 * n)) => e.card = 3).powersetCard ℓ).filter
      fun E => ∃ M : Finset (Finset (Fin (3 * n))), M ⊆ E ∧ M.card = n ∧
        (M : Set (Finset (Fin (3 * n)))).PairwiseDisjoint id).card /
    ((Finset.univ.filter fun e : Finset (Fin (3 * n)) => e.card = 3).powersetCard ℓ).card
Used by 2
Used byStatement of the upper half of Shamir's problem · Threshold for a perfect matching in a random \(3\)-uniform hypergraph

DefinitionStatement of the upper half of Shamir's problem#✓fully proved

The proposition that for every real \(\varepsilon > 0\), the probability that the uniformly random \(3\)-uniform hypergraph on \(3n\) vertices with \(\lceil (1 + \varepsilon) n \log n \rceil\) edges has a perfect matching (\(n\) pairwise disjoint edges) tends to \(1\) as \(n \to \infty\), where \(\log\) is the natural logarithm.

Erdős Problem 747 (Shamir's problem) asks for the number \(\ell(n)\) of edges at which a perfect matching becomes almost sure; this is the upper half of the answer \(\ell(n) \sim n \log n\).

def matchingAboveThreshold : Prop :=
  ∀ ε : ℝ, 0 < ε →
    Tendsto (fun n : ℕ => matchingProbability n ⌈(1 + ε) * n * Real.log n⌉₊) atTop (𝓝 1)
Uses 1 · Used by 1
Statement usesProbability of a perfect matching in a random \(3\)-uniform hypergraph
Used byKahn's theorem on Shamir's problem, upper half

DefinitionThreshold for a perfect matching in a random \(3\)-uniform hypergraph#✓fully proved

For a natural number \(n\), the threshold \(\ell_c(n)\) is the least natural number \(\ell\) such that the uniformly random \(3\)-uniform hypergraph on \(3n\) vertices with \(\ell\) edges has a perfect matching (\(n\) pairwise disjoint edges) with probability at least \(1/2\).

The set of such \(\ell\) is nonempty: with all triples present the probability is \(1\).

noncomputable def matchingThreshold (n : ℕ) : ℕ :=
  sInf {ℓ | 1 / 2 ≤ matchingProbability n ℓ}
Uses 1 · Used by 1
Statement usesProbability of a perfect matching in a random \(3\)-uniform hypergraph
Used byStatement of Shamir's problem: the matching threshold is asymptotic to \(n \log n\)

DefinitionStatement of Shamir's problem: the matching threshold is asymptotic to \(n \log n\)#✓fully proved

Let \(\ell_c(n)\) be the least number \(\ell\) such that the uniformly random \(3\)-uniform hypergraph on \(3n\) vertices with \(\ell\) edges has a perfect matching with probability at least \(1/2\). The proposition that \(\ell_c(n) / (n \log n) \to 1\) as \(n \to \infty\), where \(\log\) is the natural logarithm.

This is the answer to Erdős Problem 747 (Shamir's problem).

def matchingThresholdAsymptotic : Prop :=
  Tendsto (fun n : ℕ => (matchingThreshold n : ℝ) / (n * Real.log n)) atTop (𝓝 1)
Uses 1 · Used by 1
Statement usesThreshold for a perfect matching in a random \(3\)-uniform hypergraph
Used byKahn's theorem: the threshold in Shamir's problem is asymptotic to \(n \log n\)

TheoremKahn's theorem on Shamir's problem, upper half#●ready to prove

For every real \(\varepsilon > 0\), the probability that the uniformly random \(3\)-uniform hypergraph on \(3n\) vertices with \(\lceil (1 + \varepsilon) n \log n \rceil\) edges has a perfect matching (\(n\) pairwise disjoint edges) tends to \(1\) as \(n \to \infty\), where \(\log\) is the natural logarithm.

public theorem_wanted matchingAboveThreshold_holds : matchingAboveThreshold
Sources
  • T. F. Bloom, Erdős Problems, Problem #747, https://www.erdosproblems.com/747 (status SOLVED); resolution: J. Kahn, Asymptotics for Shamir's problem, Adv. Math. 422 (2023), Paper 109019, Theorem 1 of arXiv:1909.06834 (abstract; Theorem 1.2 in the text): for fixed r ≥ 3, ε > 0 and M > (1 + ε)(n/r) log n, the random M-edge r-graph on [n] has a perfect matching with probability → 1; Section 1: the threshold M_c, the least M for which the probability of a perfect matching is at least 1/2, satisfies M_c ∼ (n/r) log n ('In this paper we show that the asymptotics of the threshold are as expected'); erdosproblems.com/747: the threshold is ∼ n log n, https://arxiv.org/abs/1909.06834.
Uses 1
Statement usesStatement of the upper half of Shamir's problem

TheoremKahn's theorem: the threshold in Shamir's problem is asymptotic to \(n \log n\)#●ready to prove

Let \(\ell_c(n)\) be the least number \(\ell\) such that the uniformly random \(3\)-uniform hypergraph on \(3n\) vertices with \(\ell\) edges has a perfect matching with probability at least \(1/2\). Then \(\ell_c(n) / (n \log n) \to 1\) as \(n \to \infty\), where \(\log\) is the natural logarithm.

public theorem_wanted matchingThresholdAsymptotic_holds : matchingThresholdAsymptotic
Sources
  • T. F. Bloom, Erdős Problems, Problem #747, https://www.erdosproblems.com/747 (status SOLVED); resolution: J. Kahn, Asymptotics for Shamir's problem, Adv. Math. 422 (2023), Paper 109019, Theorem 1 of arXiv:1909.06834 (abstract; Theorem 1.2 in the text): for fixed r ≥ 3, ε > 0 and M > (1 + ε)(n/r) log n, the random M-edge r-graph on [n] has a perfect matching with probability → 1; Section 1: the threshold M_c, the least M for which the probability of a perfect matching is at least 1/2, satisfies M_c ∼ (n/r) log n ('In this paper we show that the asymptotics of the threshold are as expected'); erdosproblems.com/747: the threshold is ∼ n log n, https://arxiv.org/abs/1909.06834.
Uses 1
Statement usesStatement of Shamir's problem: the matching threshold is asymptotic to \(n \log n\)
4 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.