Step Graphons

Step graphons are graphons that are piecewise constant on a finite measurable partition of the probability space. They form a dense subset of the space of graphons (in cut distance) and provide the key bridge between finite graphs and graphons.

Main definitions

• MeasurablePartition - A finite measurable partition of a probability space
• Graphon.ofSimpleGraph - Construct a graphon from a finite simple graph

Main results

• Graphon.ofSimpleGraph_symm_ae - The graphon of a simple graph is symmetric a.e.
• Graphon.ofSimpleGraph_ae_mem_Icc - Values are in [0,1] a.e.

Implementation notes

The graphon ofSimpleGraph G for a simple graph G on n vertices is defined on the unit interval by partitioning [0,1] into n equal parts and setting W(x,y) = 1 if the parts containing x and y are adjacent in G, and 0 otherwise.

References

• [L. Lovász, Large Networks and Graph Limits][lovasz2012], Chapter 7

Measurable partitions

structure MeasurablePartition (α : Type u_2) [MeasurableSpace α] (μ : MeasureTheory.Measure α) : Type u_2

A finite measurable partition of a measure space.

This is a finite collection of pairwise disjoint measurable sets that cover the space almost everywhere. Used to define step graphons.

• parts : Finset (Set α)

  The parts of the partition as a finset of sets

• measurable_parts (S : Set α) : S ∈ self.parts → MeasurableSet S

  Each part is measurable

• pairwiseDisjoint : (↑self.parts).PairwiseDisjoint id

  The parts are pairwise disjoint

• ae_covers : ∀ᵐ (x : α) ∂μ, ∃ S ∈ self.parts, x ∈ S

  The parts cover the space almost everywhere

def MeasurablePartition.card {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (P : MeasurablePartition α μ) : ℕ

The number of parts in the partition.

Equations

• P.card = P.parts.card

theorem MeasurablePartition.measurableSet_part {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (P : MeasurablePartition α μ) {S : Set α} (hS : S ∈ P.parts) : MeasurableSet S

A part of the partition is measurable.

theorem MeasurablePartition.sum_measure_parts_le_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (P : MeasurablePartition α μ) [MeasureTheory.IsProbabilityMeasure μ] : ∑ S ∈ P.parts, (μ S).toReal ≤ 1

The sum of measures of partition parts is at most 1.

Since parts are pairwise disjoint, Σ μ(S) = μ(⋃ S) ≤ μ(univ) = 1.

Graphon from simple graph

noncomputable def Graphon.trivialPartition {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} : MeasurablePartition α μ

The trivial partition with just {univ} as the only part.

Equations

• Graphon.trivialPartition = { parts := {Set.univ}, measurable_parts := ⋯, pairwiseDisjoint := ⋯, ae_covers := ⋯ }

theorem Graphon.trivialPartition_card {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] : trivialPartition.parts.card = 1

def Graphon.adjIndicator {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (i j : Fin n) : ℝ

The indicator function for adjacency in a simple graph, as a real number.

Returns 1 if vertices i and j are adjacent, 0 otherwise.

Equations

• Graphon.adjIndicator G i j = if G.Adj i j then 1 else 0

theorem Graphon.adjIndicator_symm {n : ℕ} [NeZero n] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (i j : Fin n) : adjIndicator G i j = adjIndicator G j i

The adjIndicator is symmetric since adjacency is symmetric.

theorem Graphon.adjIndicator_mem_Icc {n : ℕ} [NeZero n] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (i j : Fin n) : adjIndicator G i j ∈ Set.Icc 0 1

The adjIndicator takes values in [0,1].

theorem Graphon.adjIndicator_eq_zero_or_one {n : ℕ} [NeZero n] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (i j : Fin n) : adjIndicator G i j = 0 ∨ adjIndicator G i j = 1

The adjIndicator is 0 or 1.

noncomputable def Graphon.toVertex (n : ℕ) [NeZero n] (x : ↑unitInterval) : Fin n

Map a point in the unit interval to its corresponding vertex in Fin n.

For x ∈ [0,1], returns ⌊n * x⌋ clamped to Fin n. This maps the interval [k/n, (k+1)/n) to vertex k.

Equations

• Graphon.toVertex n x = ⟨min (n - 1) ⌊↑n * ↑x⌋₊, ⋯⟩

theorem Graphon.measurable_minFloor_nat {n : ℕ} [NeZero n] : Measurable fun (x : ℝ) => min (n - 1) ⌊↑n * x⌋₊

The function x ↦ min (n-1) ⌊n*x⌋₊ as a function ℝ → ℕ is measurable.

theorem Graphon.measurable_minFloor {n : ℕ} [NeZero n] : Measurable fun (x : ℝ) => ↑(min (n - 1) ⌊↑n * x⌋₊)

The function x ↦ min (n-1) ⌊n*x⌋₊ is measurable as a real-valued function.

theorem Graphon.measurable_toVertex {n : ℕ} [NeZero n] : Measurable (toVertex n)

The toVertex function is measurable.

theorem Graphon.measurable_adjIndicator_comp_toVertex {n : ℕ} [NeZero n] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] : Measurable fun (p : ↑unitInterval × ↑unitInterval) => adjIndicator G (toVertex n p.1) (toVertex n p.2)

The function mapping pairs to adjacency indicators is measurable.

theorem Graphon.stronglyMeasurable_adjIndicator_comp_toVertex {n : ℕ} [NeZero n] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] : MeasureTheory.StronglyMeasurable fun (p : ↑unitInterval × ↑unitInterval) => adjIndicator G (toVertex n p.1) (toVertex n p.2)

The function mapping pairs to adjacency indicators is strongly measurable.

noncomputable def Graphon.ofSimpleGraph {n : ℕ} [NeZero n] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] : GraphonI

The graphon associated to a simple graph on Fin n.

Given a simple graph G on n vertices, we construct a graphon on [0,1] by:

1. Partitioning [0,1] into n equal intervals
2. Setting W(x,y) = 1 if the vertices corresponding to x and y are adjacent
3. Setting W(x,y) = 0 otherwise

This is the fundamental bridge between finite graphs and graphons. The homomorphism density t(F, W_G) equals hom(F, G) / n^|V(F)|.

Equations

• One or more equations did not get rendered due to their size.

theorem Graphon.ofSimpleGraph_apply {n : ℕ} [NeZero n] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] : ∀ᵐ (p : ↑unitInterval × ↑unitInterval) ∂MeasureTheory.volume.prod MeasureTheory.volume, ↑(ofSimpleGraph G).toAEEqFun p = adjIndicator G (toVertex n p.1) (toVertex n p.2)

The graphon of a simple graph at a point equals the adjacency indicator (a.e.).

theorem Graphon.ofSimpleGraph_bot_ae {n : ℕ} [NeZero n] : ∀ᵐ (p : ↑unitInterval × ↑unitInterval) ∂MeasureTheory.volume.prod MeasureTheory.volume, ↑(ofSimpleGraph ⊥).toAEEqFun p = 0

The graphon of the empty graph is zero almost everywhere.

theorem Graphon.ofSimpleGraph_top_ae {n : ℕ} [NeZero n] : ∀ᵐ (p : ↑unitInterval × ↑unitInterval) ∂MeasureTheory.volume.prod MeasureTheory.volume, ↑(ofSimpleGraph ⊤).toAEEqFun p = if toVertex n p.1 = toVertex n p.2 then 0 else 1

The graphon of the complete graph equals 1 off the diagonal.

Note: On the diagonal (where toVertex n p.1 = toVertex n p.2), the value is 0 because simple graphs have no self-loops.