def RandomGraph.pairToEdgeIndex (a b : ℕ) : ℕ

Linear index assigned to an unordered pair $\{a, b\}$ with $a < b$, given by $\binom{b}{2} + a$. Used to enumerate edges of the complete graph $K_n$ as elements of $\mathrm{Fin}\binom{n}{2}$.

theorem RandomGraph.pairToEdgeIndex_lt_choose {a b n : ℕ} (hab : a < b) (hbn : b < n) : pairToEdgeIndex a b < n.choose 2

The index of a pair with $a < b < n$ lies below $\binom{n}{2}$, ensuring that pairToEdgeIndex produces a valid Fin (Nat.choose n 2).

def RandomGraph.edgeIndex (n : ℕ) (i j : Fin n) (hij : ↑i < ↑j) : Fin (n.choose 2)

Edge index of the ordered pair $(i, j)$ with $i < j$ in $K_n$, as an element of $\mathrm{Fin}\binom{n}{2}$.

def RandomGraph.edgePresent (n : ℕ) (f : Fin (n.choose 2) → Bool) (i j : Fin n) : Bool

Tests whether the edge $\{i, j\}$ is present according to the bit-vector $f$ encoding a graph on $n$ vertices; returns false unless $i < j$.

noncomputable def RandomGraph.hasTriangle (n : ℕ) (f : Fin (n.choose 2) → Bool) : Bool

Decides whether the graph on $n$ vertices encoded by $f$ contains a triangle, by searching for an ordered triple $i < j < k$ with all three edges present.

noncomputable def RandomGraph.erdosRenyiTriangleProb (n : ℕ) (p : ℝ) : ℝ

The probability that $G(n, p)$ contains a triangle, computed by summing the indicator of hasTriangle weighted by the Bernoulli$(p)$ product weights over all $2^{\binom{n}{2}}$ edge configurations.

theorem RandomGraph.bernoulli_weight_nonneg {m : ℕ} (f : Fin m → Bool) (p : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1) : 0 ≤ ∏ i : Fin m, if f i = true then p else 1 - p

Each product Bernoulli weight $\prod_i (\text{if } f_i \text{ then } p \text{ else } 1-p)$ is nonnegative whenever $0 \le p \le 1$.

theorem RandomGraph.sum_bernoulli_weights (m : ℕ) (p : ℝ) : (∑ f : Fin m → Bool, ∏ i : Fin m, if f i = true then p else 1 - p) = 1

The product Bernoulli$(p)$ weights summed over ${0,1}^m$ equal $1$, by the binomial identity $(p + (1-p))^m = 1$.

theorem RandomGraph.erdosRenyiTriangleProb_nonneg (n : ℕ) (p : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1) : 0 ≤ erdosRenyiTriangleProb n p

The triangle-containment probability in $G(n, p)$ is nonnegative for $p \in [0, 1]$.

theorem RandomGraph.erdosRenyiTriangleProb_le_one (n : ℕ) (p : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1) : erdosRenyiTriangleProb n p ≤ 1

The triangle-containment probability in $G(n, p)$ is at most $1$ for $p \in [0, 1]$.

noncomputable def RandomGraph.expectedTriangles (n : ℕ) (p : ℝ) : ℝ

The expected number of triangles in $G(n, p)$, given by $\mathbb{E}[X] = \binom{n}{3} p^3$ (Proposition 4.1.2).

theorem RandomGraph.expectedTriangles_nonneg (n : ℕ) (p : ℝ) (hp : 0 ≤ p) : 0 ≤ expectedTriangles n p

The expected number of triangles in $G(n, p)$ is nonnegative when $p \ge 0$.

theorem RandomGraph.erdosRenyiTriangleProb_le_expectedTriangles (n : ℕ) (p : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1) : erdosRenyiTriangleProb n p ≤ expectedTriangles n p

First moment bound for triangles. The probability that $G(n, p)$ contains a triangle is at most the expected number of triangles $\binom{n}{3} p^3$ (Markov's inequality applied to the triangle count).

theorem RandomGraph.erdosRenyiTriangleProb_ge_one_sub_var_div_sq (n : ℕ) (p : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1) (hE : 0 < expectedTriangles n p) : erdosRenyiTriangleProb n p ≥ 1 - (expectedTriangles n p + ↑(n.choose 4) * p ^ 5) / expectedTriangles n p ^ 2

Second moment bound for triangles. Using the variance bound $\mathrm{Var}(X) \le \mathbb{E}X + \binom{n}{4} p^5$ for the triangle count $X$, the probability of at least one triangle is at least $1 - (\mathbb{E}X + \binom{n}{4} p^5) / (\mathbb{E}X)^2$.

theorem RandomGraph.expectedTriangles_le (n : ℕ) (p : ℝ) (hp : 0 ≤ p) : expectedTriangles n p ≤ (↑n * p) ^ 3 / 6

Upper bound for the expected number of triangles: $\binom{n}{3} p^3 \le (np)^3 / 6$, using $\binom{n}{3} \le n^3/3!$.

theorem RandomGraph.expectedTriangles_tendsto_zero (p : ℕ → ℝ) (hp : ∀ (n : ℕ), 0 ≤ p n) (h : Filter.Tendsto (fun (n : ℕ) => ↑n * p n) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => expectedTriangles n (p n)) Filter.atTop (nhds 0)

If $np_n \to 0$ then the expected number of triangles tends to $0$, by squeezing $\binom{n}{3} p_n^3$ between $0$ and $(np_n)^3 / 6$.

theorem RandomGraph.triangleThreshold_below (p : ℕ → ℝ) (hp : ∀ (n : ℕ), 0 ≤ p n) (probTriangle : ℕ → ℝ) (hprob_nonneg : ∀ (n : ℕ), 0 ≤ probTriangle n) (hMarkov : ∀ (n : ℕ), probTriangle n ≤ expectedTriangles n (p n)) (hpn : Filter.Tendsto (fun (n : ℕ) => ↑n * p n) Filter.atTop (nhds 0)) : Filter.Tendsto probTriangle Filter.atTop (nhds 0)

Below-threshold side of the triangle threshold. If $np_n \to 0$ and a triangle probability sequence is bounded above by the first moment, then it tends to $0$.

theorem RandomGraph.nat_cube_le_48_choose_three (n : ℕ) (hn : 4 ≤ n) : n ^ 3 ≤ 48 * n.choose 3

For $n \ge 4$, $n^3 \le 48 \binom{n}{3}$, providing a lower bound for $\binom{n}{3}$ in terms of $n^3$.

theorem RandomGraph.choose_three_ge (n : ℕ) (hn : 4 ≤ n) : ↑n ^ 3 / 48 ≤ ↑(n.choose 3)

Real-valued version of the inequality $n^3 / 48 \le \binom{n}{3}$ for $n \ge 4$.

theorem RandomGraph.expectedTriangles_ge (n : ℕ) (p : ℝ) (hp : 0 ≤ p) (hn : 4 ≤ n) : (↑n * p) ^ 3 / 48 ≤ expectedTriangles n p

Lower bound for the expected number of triangles: $(np)^3 / 48 \le \binom{n}{3} p^3$ for $n \ge 4$.

theorem RandomGraph.variance_numerator_le (n : ℕ) (p : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1) (hnp : 1 ≤ ↑n * p) : expectedTriangles n p + ↑(n.choose 4) * p ^ 5 ≤ (↑n * p) ^ 4

A bound on the variance-numerator term: when $np \ge 1$, $\binom{n}{3} p^3 + \binom{n}{4} p^5 \le (np)^4$.

theorem RandomGraph.triangle_variance_ratio_tendsto_zero (p : ℕ → ℝ) (hp : ∀ (n : ℕ), 0 ≤ p n) (hp1 : ∀ (n : ℕ), p n ≤ 1) (hpn : Filter.Tendsto (fun (n : ℕ) => ↑n * p n) Filter.atTop Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => (expectedTriangles n (p n) + ↑(n.choose 4) * p n ^ 5) / expectedTriangles n (p n) ^ 2) Filter.atTop (nhds 0)

If $np_n \to \infty$, then the variance-over-squared-mean ratio for the triangle count tends to $0$, the key second-moment input for the above-threshold direction.

theorem RandomGraph.triangleThreshold_above (p : ℕ → ℝ) (hp : ∀ (n : ℕ), 0 ≤ p n) (hp1 : ∀ (n : ℕ), p n ≤ 1) (hpn : Filter.Tendsto (fun (n : ℕ) => ↑n * p n) Filter.atTop Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => erdosRenyiTriangleProb n (p n)) Filter.atTop (nhds 1)

Above-threshold side of the triangle threshold (Theorem 4.1.11, second part). If $np_n \to \infty$, then $\mathbb{P}(G(n, p_n) \text{ contains a triangle}) \to 1$.

theorem RandomGraph.triangle_free_whp_gnp (p : ℕ → ℝ) (hp : ∀ (n : ℕ), 0 ≤ p n) (hp1 : ∀ (n : ℕ), p n ≤ 1) (hpn : Filter.Tendsto (fun (n : ℕ) => ↑n * p n) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => erdosRenyiTriangleProb n (p n)) Filter.atTop (nhds 0)

Triangle-free w.h.p. side of Theorem 4.1.11. If $np_n \to 0$, then $\mathbb{P}(G(n, p_n) \text{ contains a triangle}) \to 0$, i.e. $G(n, p_n)$ is triangle-free with high probability.