noncomputable def Thresholds.directedEdgesInSubset {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj] (S : Finset V) : ℕ

The number of ordered pairs $(u, v)$ in $S \times S$ with $u \neq v$ and $u \sim_H v$. This is twice the number of edges in the induced subgraph $H[S]$.

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

The maximum edge-to-vertex ratio over nonempty subsets of $V(H)$, i.e. $m(H) = \max_{S \ne \emptyset} |E(H[S])| / |S|$.

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

The probability that $G(n, p)$ contains $H$ as a (not necessarily induced) subgraph, computed by summing Bernoulli edge weights over all graphs $G$ on $n$ vertices that admit an injective graph homomorphism from $H$.

theorem Thresholds.indicator_exists_le_sum {V : Type u_1} [Fintype V] (n : ℕ) (H : SimpleGraph V) [DecidableRel H.Adj] (G : SimpleGraph (Fin n)) : (if ∃ (f : V ↪ Fin n), ∀ (v w : V), H.Adj v w → G.Adj (f v) (f w) then 1 else 0) ≤ ∑ f : V ↪ Fin n, if ∀ (v w : V), H.Adj v w → G.Adj (f v) (f w) then 1 else 0

The indicator of "there exists an injective homomorphism $H \hookrightarrow G$" is bounded by the sum of indicators over all injections, since at least one injection works whenever the existential holds.

theorem Thresholds.restricted_bernoulli_sum_le {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj] [Fintype ↑H.edgeSet] (n : ℕ) (p : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1) (f : V ↪ Fin n) : ∑ G : SimpleGraph (Fin n), (if ∀ (v w : V), H.Adj v w → G.Adj (f v) (f w) then 1 else 0) * (p ^ Fintype.card ↑G.edgeSet * (1 - p) ^ (n.choose 2 - Fintype.card ↑G.edgeSet)) ≤ p ^ Fintype.card ↑H.edgeSet

The Bernoulli probability that $G$ contains the image of $H$ under a fixed injection $f : V(H) \hookrightarrow [n]$ is at most $p^{|E(H)|}$, since all $|E(H)|$ edges of $H$ must appear independently.

theorem Thresholds.densest_subgraph_bound {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (H : SimpleGraph V) [DecidableRel H.Adj] [Fintype ↑H.edgeSet] (hH : 0 < maxEdgeVertexRatio H) : ∃ (k : ℕ), 0 < k ∧ ∀ (n : ℕ), 1 ≤ n → ∀ (p : ℝ), |p| ≤ 1 → 0 ≤ probContainsSubgraph H n p ∧ probContainsSubgraph H n p ≤ |p / ↑n ^ (-1 / maxEdgeVertexRatio H)| ^ k

A densest-subgraph first-moment bound: there exists $k > 0$ depending on $H$ such that the probability of containing $H$ is bounded by $|p / n^{-1/m(H)}|^k$, the key nonnegativity-plus-upper-bound estimate underlying the first moment direction.

theorem Thresholds.first_moment_zero_statement {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (H : SimpleGraph V) [DecidableRel H.Adj] [Fintype ↑H.edgeSet] (hH : 0 < maxEdgeVertexRatio H) (p : ℕ → ℝ) (hp : Filter.Tendsto (fun (n : ℕ) => p n / ↑n ^ (-1 / maxEdgeVertexRatio H)) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => probContainsSubgraph H n (p n)) Filter.atTop (nhds 0)

First moment side of Bollobás's threshold theorem. If $p_n / n^{-1/m(H)} \to 0$, then the probability that $G(n, p_n)$ contains $H$ as a subgraph tends to $0$.

theorem Thresholds.second_moment_one_statement {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (H : SimpleGraph V) [DecidableRel H.Adj] [Fintype ↑H.edgeSet] (hH : 0 < maxEdgeVertexRatio H) (p : ℕ → ℝ) (hp : Filter.Tendsto (fun (n : ℕ) => p n / ↑n ^ (-1 / maxEdgeVertexRatio H)) Filter.atTop Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => probContainsSubgraph H n (p n)) Filter.atTop (nhds 1)

Second moment side of Bollobás's threshold theorem. If $p_n / n^{-1/m(H)} \to \infty$, then the probability that $G(n, p_n)$ contains $H$ as a subgraph tends to $1$.

theorem Thresholds.bollobas_threshold {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (H : SimpleGraph V) [DecidableRel H.Adj] [Fintype ↑H.edgeSet] (hH : 0 < maxEdgeVertexRatio H) : SubgraphThreshold.IsSubgraphThreshold (probContainsSubgraph H) fun (n : ℕ) => ↑n ^ (-1 / maxEdgeVertexRatio H)

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