Sampling Random Graphs from Graphons #
This file defines the finite distribution of the W-random graph G(k, W) and the
expected edge density, WITHOUT introducing random variables: the probability mass of
each graph is defined directly as an integral.
Main definitions #
Graphon.sampleMass— the probability thatG(k, W)equals a given graphG:∫ x, ∏_{e ∈ E(G)} W(xᵢ,xⱼ) · ∏_{e ∉ E(G)} (1 − W(xᵢ,xⱼ))Graphon.sampleGraphExpectedDensity— Expected edge density of sampled graph
Main results #
Graphon.sampleMass_nonneg— masses are nonnegativeGraphon.sampleMass_sum_eq_one— masses sum to 1 over all graphs onFin kGraphon.sampleMass_eq_sum_homDensity— each mass is a finite signed sum of homomorphism densities of graphs onFin k(inclusion–exclusion)Graphon.sampleMass_close_of_homDensity_close— hom-density closeness onFin kcontrols each mass differenceGraphon.sampleDistribution_tv_close_of_homDensity_close— hence total-variation closeness of the sampled graph distributions (the bridge for the BCLSV sampling route toheadline_parameter_selection)Graphon.sampleGraphExpectedDensity_eq— Expected density equals ∫∫ WGraphon.sampleGraphExpectedDensity_mem_Icc— Expected density is in [0, 1]
Implementation notes #
The sampling process for G(n, W) is:
- Sample n i.i.d. points x₁, ..., xₙ uniformly from [0,1]
- 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 is proved in Graphon/SamplingConcentration.lean
/ SamplingPointwise.lean / SamplingRounding.lean, culminating in the First Sampling
Lemma (Graphon/SamplingLemma.lean); convergence in Graphon/Convergence.lean.
References #
- [L. Lovász, Large Networks and Graph Limits][lovasz2012], Section 10.2-10.3
Sampling definition #
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.
Instances For
The expected edge density equals the double integral of the graphon.
The expected edge density is in [0,1].
The sampled graph distribution #
The distribution of the W-random graph G(k, W) on Fin k, given by explicit
probability masses. Everything here is finite algebra plus integrals: no random
variables, no concentration.
A.e. transfer from the product measure to a pair of distinct sampled coordinates:
if Φ holds μ.prod μ-a.e., it holds a.e. at (x a, x b) for i.i.d. samples x and
a ≠ b. (Generalized from SamplingPointwise — needs only a probability measure, no
standard-Borel or atomlessness hypotheses.)
The integrand of the sampled-graph mass: edges of G contribute W, non-edges
contribute 1 − W.
Equations
Instances For
The sampled graph distribution: the probability that the W-random graph
G(k, W) equals G. Sample k i.i.d. positions, then include each pair {i, j} as an
edge independently with probability W(xᵢ, xⱼ); integrating out the positions gives
this mass directly, with no random-variable formalism.
Equations
- W.sampleMass G = ∫ (x : Fin k → α), W.sampleIntegrand G x ∂MeasureTheory.Measure.pi fun (x : Fin k) => μ
Instances For
The sampled-graph integrand is integrable (as a finite signed sum of integrable hom-density integrands). Public: used by the concentration scaffold.
Mass expansion: each sampled-graph mass is a finite signed sum of homomorphism
densities of graphs on Fin k (inclusion–exclusion over the non-edges of G).
All edge evaluations over ⊤ lie in [0,1] almost everywhere (public: used by the
concentration scaffold for a.e. nonnegativity of conditional masses).
Sampled-graph masses are nonnegative.
Pointwise: the sampled-graph integrands sum to 1 over all graphs on Fin k
(public: this is the conditional-distribution normalization used by the concentration
scaffold).
The sampled-graph masses form a probability distribution: they sum to 1.
The forward Möbius / supergraph-mass identity (issue #20) #
homDensity F W = ∑_{G ⊇ F} sampleMass W G: the homomorphism density of F is exactly
the probability that the sampled graph contains every edge of F. This is the forward
companion of the inclusion–exclusion expansion sampleMass_eq_sum_homDensity above.
Proof route (vetted 2026-07-10): at fixed vertex positions, supergraphs of F are in
bijection with subsets of the optional edges ⊤.edgeFinset \ F.edgeFinset; summing the
Bernoulli integrand over the Boolean cube via Finset.prod_add collapses each optional
factor to w e + (1 - w e) = 1, leaving the plain edge product of F.
The forward Möbius / supergraph-mass identity (filtered form): the total sample
mass of the supergraphs of F is exactly the homomorphism density of F. Accepts an
ambient [DecidableRel F.Adj] (bridged to the classical core by
homDensity_congr_decRel).
The forward Möbius / supergraph-mass identity (issue #20 orientation):
t(F, W) = ∑_{G ⊇ F} sampleMass W G on a common labeled vertex set. Accepts an ambient
[DecidableRel F.Adj].
Mass closeness from hom-density closeness: if all hom densities of graphs on
Fin k agree within δ, each sampled-graph mass agrees within 2^(k·k) · δ.
Total-variation closeness from hom-density closeness — the deliverable bridge
for the BCLSV sampling route: if all hom densities of graphs on Fin k agree within
δ, the sampled graph distributions of U and W agree within 4^(k·k) · δ in
(twice the) total variation distance.
Event extraction from total variation: any event's probabilities under the two sampled distributions differ by at most the (summed) total variation distance.