Thresholds and expectation thresholds

DefinitionWeakly \(p\)-small families#✓fully proved

Let \(X\) be a finite set, \(p \in [0, 1]\), and \(\mathcal F\) a family of subsets of \(X\). Then \(\mathcal F\) is weakly \(p\)-small if there is a function \(g\) from subsets of \(X\) to the nonnegative reals such that \(\sum_{S \subseteq T} g(S) \ge 1\) for every \(T \in \mathcal F\) and \(\sum_{S \subseteq X} g(S)\, p^{|S|} \le 1/2\).

def IsWeaklySmall {X : Type*} [Fintype X] (p : I) (𝓕 : Set (Set X)) : Prop :=
  ∃ g : Set X → ℝ≥0, (∀ T ∈ 𝓕, ∑ S with S ⊆ T, g S ≥ 1) ∧ ∑ S, g S * (p : ℝ) ^ S.ncard ≤ 2⁻¹

Used by 1

Used byThe fractional expectation-threshold \(q_f(\mathcal F)\)

DefinitionThe threshold \(p_c(\mathcal F)\)#✓fully proved

For a set \(X\) and \(p \in [0, 1]\), let \(\mu_p\) be the \(p\)-biased product measure on subsets of \(X\), under which each element of \(X\) lies in the random subset independently with probability \(p\). For a family \(\mathcal F\) of subsets of \(X\), \(p_c(\mathcal F)\) is some \(p \in [0, 1]\) with \(\mu_p(\mathcal F) = 1/2\) if such a \(p\) exists, and \(0\) otherwise.

When \(X\) is finite and \(\mathcal F\) is increasing, nonempty and not the family of all subsets of \(X\), such a \(p\) exists and is unique; it is the threshold of \(\mathcal F\).

noncomputable def p_c {X : Type*} (𝓕 : Set (Set X)) : I :=
  if h : ∃ p, setBer(univ, p).real (𝓕 : Set (Set X)) = 2⁻¹ then Classical.choose h else 0

Used by 1

Used byThresholds versus fractional expectation-thresholds

DefinitionThe fractional expectation-threshold \(q_f(\mathcal F)\)#✓fully proved

For a family \(\mathcal F\) of subsets of a finite set \(X\), \(q_f(\mathcal F)\) is the supremum, in \([0, 1]\), of the set of all \(p \in [0, 1]\) such that \(\mathcal F\) is weakly \(p\)-small; it is \(0\) if there is no such \(p\).

noncomputable def q_f {X : Type*} [Fintype X] (𝓕 : Set (Set X)) : I :=
  sSup {p | IsWeaklySmall p 𝓕}

Uses 1 · Used by 1

Statement usesWeakly \(p\)-small families

Used byThresholds versus fractional expectation-thresholds

DefinitionSize of a largest minimal element, \(\ell(\mathcal F)\)#✓fully proved

For a family \(\mathcal F\) of subsets of a set \(X\), \(\ell(\mathcal F)\) is the largest cardinality of a minimal element of \(\mathcal F\) (minimal with respect to inclusion), a natural number.

By convention \(\ell(\mathcal F) = 0\) when \(\mathcal F\) has no minimal element or when the cardinalities of its minimal elements are unbounded, and an infinite set counts as having cardinality \(0\).

noncomputable def l {X : Type*} (𝓕 : Set (Set X)) : ℕ :=
  ⨆ (A : 𝓕) (_ : IsMin A), (A : Set X).ncard

Used by 1

Used byThresholds versus fractional expectation-thresholds

DefinitionThe constant of the Frankston–Kahn–Narayanan–Park theorem#●ready to state

A real number \(K\), not yet specified, that is to serve as the universal constant in the bound of the threshold of an increasing family by \(K\) times its fractional expectation-threshold times the logarithm of the size of its largest minimal element.

public def_wanted K : ℝ

Sources

• K. Frankston, J. Kahn, B. Narayanan, and J. Park, Thresholds versus fractional expectation-thresholds, Annals of Math, 194 (2) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_fractional_expectation_thresholds of the lean-eval benchmark.

Used by 1

Used byThresholds versus fractional expectation-thresholds

TheoremThresholds versus fractional expectation-thresholds#●statement formalized

Let \(K\) be the universal real constant still to be supplied. For every finite set \(X\) and every increasing family \(\mathcal F\) of subsets of \(X\) (closed under taking supersets) with \(\ell(\mathcal F) \ge 2\), where \(\ell(\mathcal F)\) is the size of a largest minimal element of \(\mathcal F\),

\[p_c(\mathcal F) \le K \, q_f(\mathcal F) \log \ell(\mathcal F),\]

where \(p_c\) is the threshold, \(q_f\) the fractional expectation-threshold and \(\log\) the natural logarithm.

The hypothesis \(\ell(\mathcal F) \ge 2\) is not explicit in the paper but is needed: if \(\ell(\mathcal F) = 1\) then \(\log \ell(\mathcal F) = 0\), while \(p_c(\mathcal F) \in (0, 1)\), so the inequality cannot hold.

public theorem_wanted theorem_1_1 (X : Type*) [Fintype X] (𝓕 : Set (Set X)) (h𝓕 : IsUpperSet 𝓕)
    (hl𝓕 : 2 ≤ l 𝓕) : p_c 𝓕 ≤ ❰K❱ * q_f 𝓕 * Real.log (l 𝓕)

Sources

• K. Frankston, J. Kahn, B. Narayanan, and J. Park, Thresholds versus fractional expectation-thresholds, Annals of Math, 194 (2) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_fractional_expectation_thresholds of the lean-eval benchmark.

Uses 4

Statement usesThe constant of the Frankston–Kahn–Narayanan–Park theorem · Size of a largest minimal element, \(\ell(\mathcal F)\) · The threshold \(p_c(\mathcal F)\) · The fractional expectation-threshold \(q_f(\mathcal F)\)

4 fully proved1 statement formalized1 ready to state

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.