Sampling Random Graphs from Graphons

This file defines expected edge density for graphon sampling. Concentration bounds and the full random graph sampling API are future work.

Experimental: Concentration bounds and the full random graph sampling API are future work.

Main definitions

• Graphon.sampleGraphExpectedDensity — Expected edge density of sampled graph

Main results

• Graphon.sampleGraphExpectedDensity_eq — Expected density equals ∫∫ W
• Graphon.sampleGraphExpectedDensity_mem_Icc — Expected density is in [0, 1]

Implementation notes

The sampling process for G(n, W) is:

1. Sample n i.i.d. points x₁, ..., xₙ uniformly from [0,1]
2. Connect vertices i and j (i < j) independently with probability W(xᵢ, xⱼ)

This is a two-level randomness: first the positions, then the edges.

The key result established here is that the expected edge density equals the integral of the graphon. Concentration and convergence results are future work.

References

• [L. Lovász, Large Networks and Graph Limits][lovasz2012], Section 10.2-10.3

Sampling definition

noncomputable def Graphon.sampleGraphExpectedDensity {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) : ℝ

The expected edge density of a graph sampled from a graphon.

For a graphon W, if we sample n points x₁,...,xₙ and connect i~j with probability W(xᵢ,xⱼ), the expected edge density is ∫∫ W(x,y) dμ(x) dμ(y).

Note: This is the expected density over both the position randomness and the edge randomness.

Equations

• W.sampleGraphExpectedDensity = ∫ (p : α × α), ↑W.toAEEqFun p ∂μ.prod μ

theorem Graphon.sampleGraphExpectedDensity_eq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) : W.sampleGraphExpectedDensity = ∫ (x : α), ∫ (y : α), ↑W.toAEEqFun (x, y) ∂μ ∂μ

The expected edge density equals the double integral of the graphon.

theorem Graphon.sampleGraphExpectedDensity_mem_Icc {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) : W.sampleGraphExpectedDensity ∈ Set.Icc 0 1

The expected edge density is in [0,1].