def GraphProperty.IsMonotone (μ : ℕ → ℝ → ℝ) : Prop

A family $(\mu_n)$ of edge-probability-indexed quantities is monotone if, for each $n$, $p \mapsto \mu_n(p)$ is nondecreasing on $[0, 1]$.

def GraphProperty.IsIsomorphismInvariant (μ : ℕ → ℝ → ℝ) : Prop

A family $(\mu_n)$ comes from an isomorphism-invariant monotone graph property if there exist decidable, permutation-invariant, upwards-closed predicates $\mathrm{prop}_n$ on edge sets such that $\mu_n(p)$ equals the probability under $G(n, p)$ that the edge set satisfies $\mathrm{prop}_n$.

theorem GraphProperty.coarse_threshold_rational_exponent (μ : ℕ → ℝ → ℝ) (r : ℕ → ℝ) (hMono : IsMonotone μ) (hInv : IsIsomorphismInvariant μ) (hCoarse : Threshold.IsCoarseThreshold μ r) : ∃ (k : ℕ) (parts : Fin k → Set ℕ) (α : Fin k → ℚ), (∀ (n : ℕ), ∃ (i : Fin k), n ∈ parts i) ∧ (∀ (i j : Fin k), i ≠ j → Disjoint (parts i) (parts j)) ∧ (∀ (i : Fin k), 0 < α i) ∧ ∀ (i : Fin k), Asymptotics.IsEquivalent (Filter.atTop ⊓ Filter.principal (parts i)) (fun (n : ℕ) => r n) fun (n : ℕ) => ↑n ^ (-↑(α i))

Friedgut's sharp threshold theorem (Corollary 4.3.15): every monotone, isomorphism-invariant graph property with a coarse threshold has threshold function asymptotic to $n^{-\alpha_i}$ for a rational exponent $\alpha_i$ on each part of a finite partition of $\mathbb{N}$.