noncomputable def MaxDegreeRandomGraph.numGraphsMaxDegBounded (n : ℕ) : ℕ

The number of labeled simple graphs on $\{1, \dots, n\}$ whose maximum degree is at most $\lfloor n/2 \rfloor$.

noncomputable def MaxDegreeRandomGraph.numGraphsTotal (n : ℕ) : ℕ

Total number of labeled simple graphs on $n$ vertices, equal to $2^{\binom{n}{2}}$.

noncomputable def MaxDegreeRandomGraph.probMaxDegAtMostHalf (n : ℕ) : ℝ

Probability that the uniform random labeled graph $G(n, 1/2)$ has maximum degree at most $\lfloor n/2 \rfloor$.

theorem riordan_selby_maxdeg : have c := Real.exp (sSup (Set.range MaxDegreeNormalLabels.g)); 1 / 2 < c ∧ c < 1 ∧ Filter.Tendsto (fun (n : ℕ) => MaxDegreeRandomGraph.probMaxDegAtMostHalf n ^ (1 / ↑n)) Filter.atTop (nhds c)

Theorem 7.2.5 (Riordan-Selby 2000). The probability that the random graph $G(n, 1/2)$ has maximum degree at most $\lfloor n/2 \rfloor$ satisfies $\mathbb{P}^{1/n} \to c$ for some constant $c \in (1/2, 1)$, where $c$ is the exponential of the supremum of the explicit functional $g$ defined on the normal-labels model.

theorem normal_model_maxdeg : ∃ (c : ℝ), 1 / 2 < c ∧ c < 1 ∧ Filter.Tendsto (fun (n : ℕ) => MaxDegreeNormalLabels.prob_all_nonpos n ^ (1 / ↑n)) Filter.atTop (nhds c)

Proposition 7.2.6 (max degree with normal labels). In the surrogate model where vertices receive i.i.d. normal labels and an edge is kept if both endpoints have nonpositive labels, the probability of "all labels nonpositive" raised to the power $1/n$ converges to some constant $c \in (1/2, 1)$.