noncomputable def TriangleUpperTail.erdosRenyiTriangleUpperTailProb (n : ℕ) (p δ : ℝ) : ℝ

Probability that the Erdős–Rényi random graph $G(n, p)$ has at least $(1 + \delta) \binom{n}{3} p^3$ triangles (the upper tail event).

theorem TriangleUpperTail.erdosRenyiTriangleUpperTailProb_nonneg (n : ℕ) (p δ : ℝ) (hp : 0 < p) (hp1 : p < 1) (hδ : 0 < δ) : 0 ≤ erdosRenyiTriangleUpperTailProb n p δ

The triangle upper-tail probability is nonnegative.

theorem TriangleUpperTail.erdosRenyiTriangleUpperTailProb_le_one (n : ℕ) (p δ : ℝ) (hp : 0 < p) (hp1 : p < 1) (hδ : 0 < δ) : erdosRenyiTriangleUpperTailProb n p δ ≤ 1

The triangle upper-tail probability is at most $1$.

theorem TriangleUpperTail.erdosRenyiTriangleUpperTailProb_pos (n : ℕ) (p δ : ℝ) (hp : 0 < p) (hp1 : p < 1) (hδ : 0 < δ) : 0 < erdosRenyiTriangleUpperTailProb n p δ

For $0 < p < 1$ and $\delta > 0$, the triangle upper-tail probability is strictly positive (the event is achievable, e.g. by the complete graph).

noncomputable def TriangleUpperTail.negLogProbTriangleUpperTail (n : ℕ) (p δ : ℝ) : ℝ

Rate function $-\log \mathbb{P}[\text{triangle upper tail}]$ associated with the upper-tail event for $G(n, p)$.

theorem TriangleUpperTail.harel_mousset_samotij_upper_regime (p : ℕ → ℝ) (δ : ℝ) (hδ : 0 < δ) (hp_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < p n) (hp_lt_one : ∀ᶠ (n : ℕ) in Filter.atTop, p n < 1) (hp_lower : Filter.Tendsto (fun (n : ℕ) => p n * ↑n ^ (1 / 2)) Filter.atTop Filter.atTop) (hp_upper : Filter.Tendsto p Filter.atTop (nhds 0)) : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => negLogProbTriangleUpperTail n (p n) δ) fun (n : ℕ) => min (δ / 3) (δ ^ (2 / 3) / 2) * ↑n ^ 2 * p n ^ 2 * Real.log (1 / p n)

Theorem 8.2.5 (Harel–Mousset–Samotij, upper regime). When $p \to 0$ with $p \cdot n^{1/2} \to \infty$, the rate function is asymptotically equivalent to $\min(\delta/3, \delta^{2/3}/2) \cdot n^2 p^2 \log(1/p)$.

theorem TriangleUpperTail.harel_mousset_samotij_lower_regime (p : ℕ → ℝ) (δ : ℝ) (hδ : 0 < δ) (hp_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < p n) (hp_lower : Filter.Tendsto (fun (n : ℕ) => p n * ↑n / Real.log ↑n) Filter.atTop Filter.atTop) (hp_upper : Filter.Tendsto (fun (n : ℕ) => p n * ↑n ^ (1 / 2)) Filter.atTop (nhds 0)) : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => negLogProbTriangleUpperTail n (p n) δ) fun (n : ℕ) => δ ^ (2 / 3) / 2 * ↑n ^ 2 * p n ^ 2 * Real.log (1 / p n)

Theorem 8.2.5 (Harel–Mousset–Samotij, lower regime). When $p \cdot n / \log n \to \infty$ but $p \cdot n^{1/2} \to 0$, the rate function is asymptotically equivalent to $\frac{\delta^{2/3}}{2} \cdot n^2 p^2 \log(1/p)$.