noncomputable def MaxDegreeNormalLabels.std_normal_cdf (x : ℝ) : ℝ

Standard normal cumulative distribution function: $\Phi(x) = \mathbb{P}(Z \leq x)$ for $Z \sim \mathcal{N}(0, 1)$.

noncomputable def MaxDegreeNormalLabels.g (y : ℝ) : ℝ

Auxiliary functional appearing in Proposition 7.2.6: $g(y) = -y^2 / 2 + \log \Phi(y)$.

noncomputable def MaxDegreeNormalLabels.prob_all_nonpos (n : ℕ) : ℝ

Probability (integral representation) that in a graph with i.i.d. normal edge labels, the labelled-degree-sums at all $n$ vertices are simultaneously nonpositive.

theorem MaxDegreeNormalLabels.tendsto_log_prob_all_nonpos_div : Filter.Tendsto (fun (n : ℕ) => 1 / ↑n * Real.log (prob_all_nonpos n)) Filter.atTop (nhds (sSup (Set.range g)))

Proposition 7.2.6: As $n \to \infty$, $\frac{1}{n} \log \mathbb{P}(\text{all signed degree sums} \leq 0)$ converges to $\sup_y g(y)$, where $g$ is the functional above.