def SubgraphThreshold.IsSubgraphThreshold (probContainsH : ℕ → ℝ → ℝ) (q : ℕ → ℝ) : Prop

A function $q : \mathbb{N} \to \mathbb{R}$ is a threshold for the property of containing $H$ if for any sequence $p_n$ with $p_n / q_n \to 0$ the probability $\mathbb{P}(H \subseteq G(n, p_n)) \to 0$, and if $p_n / q_n \to \infty$ then this probability tends to $1$.

noncomputable def SubgraphThreshold.maxDensity {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj] [Nonempty V] : ℝ

The maximum edge density of a graph $H$, defined as $m(H) = \max_{S \subseteq V(H), S \ne \emptyset} \frac{|E(H[S])|}{|S|}$, where the numerator counts edges in the induced subgraph on $S$.

noncomputable def SubgraphThreshold.probContainsSubgraph {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj] (n : ℕ) (p : ℝ) : ℝ

The probability that the Erdős–Rényi random graph $G(n, p)$ contains $H$ as a subgraph, computed as the sum over all graphs $G$ on $n$ vertices weighted by their Bernoulli edge probabilities, with indicator of containing an injective homomorphism from $H$.

noncomputable def SubgraphThreshold.thresholdFunction {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj] [Nonempty V] (n : ℕ) : ℝ

The conjectural threshold function $q(n) = n^{-1/m(H)}$ for a subgraph $H$, where $m(H)$ is the maximum edge density of $H$.

theorem SubgraphThreshold.subgraphThreshold_answer {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (H : SimpleGraph V) [DecidableRel H.Adj] [Fintype ↑H.edgeSet] (hH : 0 < maxDensity H) : IsSubgraphThreshold (probContainsSubgraph H) (thresholdFunction H)

Bollobás 1981 threshold theorem (Theorem 4.2.10). For any graph $H$ with positive maximum density $m(H) > 0$, the function $n^{-1/m(H)}$ is a threshold for the property that $G(n, p)$ contains $H$ as a subgraph.