structure RandomGraphs.Edge (n : ℕ) : Type

An (unordered) edge of $K_n$ encoded as an ordered pair $\text{src} < \text{dst}$ of vertices in $\text{Fin } n$.

• src : Fin n
• dst : Fin n
• hlt : self.src < self.dst

def RandomGraphs.instDecidableEqEdge.decEq {n✝ : ℕ} (x✝ x✝¹ : Edge n✝) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance RandomGraphs.instDecidableEqEdge {n✝ : ℕ} : DecidableEq (Edge n✝)

@[reducible, inline]

abbrev RandomGraphs.Config (n : ℕ) : Type

A configuration of $G(n, p)$: a Boolean assignment to each edge indicating whether it is present.

structure RandomGraphs.Triple (n : ℕ) : Type

An ordered triple of vertices $i < j < k$ in $\text{Fin } n$, used to index potential triangles in $K_n$.

• i : Fin n
• j : Fin n
• k : Fin n
• hij : self.i < self.j
• hjk : self.j < self.k

@[implicit_reducible]

instance RandomGraphs.instDecidableEqTriple {n✝ : ℕ} : DecidableEq (Triple n✝)

def RandomGraphs.instDecidableEqTriple.decEq {n✝ : ℕ} (x✝ x✝¹ : Triple n✝) : Decidable (x✝ = x✝¹)

def RandomGraphs.Triple.eij {n : ℕ} (t : Triple n) : Edge n

The edge $\{i, j\}$ of the triple $\{i, j, k\}$.

def RandomGraphs.Triple.eik {n : ℕ} (t : Triple n) : Edge n

The edge $\{i, k\}$ of the triple $\{i, j, k\}$.

def RandomGraphs.Triple.ejk {n : ℕ} (t : Triple n) : Edge n

The edge $\{j, k\}$ of the triple $\{i, j, k\}$.

def RandomGraphs.ConfigLE {n : ℕ} (G H : Config n) : Prop

Pointwise containment of edge configurations: $G \leq H$ iff every edge of $G$ is in $H$.

def RandomGraphs.IsDecreasing {n : ℕ} (A : Set (Config n)) : Prop

An event $A$ on configurations is decreasing (monotone-down) if removing edges preserves membership: $G \in A$ and $H \leq G$ implies $H \in A$.

def RandomGraphs.notTriangleEvent {n : ℕ} (t : Triple n) : Set (Config n)

The event that the triangle on the triple $t = \{i, j, k\}$ is absent in $G$.

def RandomGraphs.triangleFreeEvent (n : ℕ) : Set (Config n)

The event that $G$ is triangle-free: no triple $\{i, j, k\}$ spans a triangle.

theorem RandomGraphs.notTriangleEvent_isDecreasing {n : ℕ} (t : Triple n) : IsDecreasing (notTriangleEvent t)

The event "the triangle on $t$ is absent" is decreasing in $G$.

def RandomGraphs.bernoulliWeight {n : ℕ} [Fintype (Edge n)] (p : ℝ) (G : Config n) : ℝ

Weight assigned to a configuration $G$ under $G(n, p)$: $\prod_{e} p^{G_e} (1 - p)^{1 - G_e}$.

def RandomGraphs.BProb {n : ℕ} [Fintype (Edge n)] [Fintype (Config n)] (p : ℝ) (A : Set (Config n)) [DecidablePred fun (x : Config n) => x ∈ A] : ℝ

Probability of an event $A$ under the $G(n, p)$ Bernoulli product measure: $\mathbb{P}_p(A) = \sum_{G \in A} \text{bernoulliWeight}(p, G)$.

theorem RandomGraphs.harris_inequality_decreasing {n : ℕ} [Fintype (Edge n)] [Fintype (Config n)] (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {ι : Type u_1} [Fintype ι] (A : ι → Set (Config n)) [(i : ι) → DecidablePred fun (x : Config n) => x ∈ A i] [DecidablePred fun (x : Config n) => x ∈ ⋂ (i : ι), A i] (hA : ∀ (i : ι), IsDecreasing (A i)) : BProb p (⋂ (i : ι), A i) ≥ ∏ i : ι, BProb p (A i)

Corollary 7.1.6 (decreasing form): For finitely many decreasing events $A_i$ in $G(n, p)$, $\mathbb{P}_p\!\left(\bigcap_i A_i\right) \geq \prod_i \mathbb{P}_p(A_i)$.

theorem RandomGraphs.prob_notTriangle_eq {n : ℕ} [Fintype (Edge n)] [Fintype (Config n)] (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (t : Triple n) [DecidablePred fun (x : Config n) => x ∈ notTriangleEvent t] : BProb p (notTriangleEvent t) = 1 - p ^ 3

The probability that a specific triple of vertices does not form a triangle in $G(n, p)$ is exactly $1 - p^3$.

theorem RandomGraphs.card_triple_eq_choose (n : ℕ) [Fintype (Triple n)] : Fintype.card (Triple n) = n.choose 3

The number of ordered triples $i < j < k$ in $\text{Fin } n$ equals $\binom{n}{3}$.

theorem RandomGraphs.theorem_7_2_2 (n : ℕ) (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (_hn : 3 ≤ n) [Fintype (Edge n)] [Fintype (Config n)] [Fintype (Triple n)] [DecidablePred fun (x : Config n) => x ∈ triangleFreeEvent n] [(t : Triple n) → DecidablePred fun (x : Config n) => x ∈ notTriangleEvent t] [DecidablePred fun (x : Config n) => x ∈ ⋂ (t : Triple n), notTriangleEvent t] : BProb p (triangleFreeEvent n) ≥ (1 - p ^ 3) ^ n.choose 3

Theorem 7.2.2: For the Erdős-Rényi random graph $G(n, p)$, $\mathbb{P}(G(n, p) \text{ is triangle-free}) \geq (1 - p^3)^{\binom{n}{3}}$.