The joint sampling law of a graphon

The finite sampling laws sampleGraph W n are one probability measure for each n, on a different space each time, and nothing in that family couples them: the separate laws relate only through pushforwards, and do not themselves supply the common random object a samplewise or almost-sure statement about the samples as n grows needs. This file builds that object: an infinite W-random graph on the label set ℕ, sampled once, from which every finite sample is read off by restriction.

The randomness is explicit. A position x i is drawn from the graphon's carrier independently for each label i, and an independent coin u e is drawn for each unordered pair e from the uniform law on the unit interval, TauCeti.Probability.uniformMeasure 0 1; the pair {i, j} becomes an edge exactly when its coin falls below the graphon value at the two positions. Both families are infinite products of probability measures, so MeasureTheory.Measure.infinitePi carries them, and the resulting law on SimpleGraph ℕ uses the adjacency sigma-algebra Mathlib already provides.

The finite-marginal identification is the theorem of the file. For a fixed pattern H on Fin n the event that the window of the infinite graph equals H is a box: it constrains the coin of each pair of distinct labels below n to an interval — below the graphon value for the pairs H joins, above it for the pairs it does not — and constrains nothing else. The coin product of that box is the conditional mass sampleIntegrand W H at the sampled positions, and averaging over the positions is sampleMass W H.

Main definitions

• TauCeti.DenseGraphLimits.infiniteSampleLaw — its law, the joint sampling object.

Main results

• infiniteSampleLaw_map_restrictFin — every finite sampling law is a window of the joint law, along the window map SimpleGraph.restrictFin.

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §10.1.
• S. Janson, Graphons, cut norm and distance, couplings and rearrangements, NYJM Monographs 4 (2013), §7.
• C. Freer, cameronfreer/graphon at commit 6eccca5bbe5c9df46d7129bf59575b8b9b1d6699, Apache-2.0, Graphon/InfiniteSampler.lean. The same one-space sampler — i.i.d. positions and one independent uniform coin per unordered pair, both carried by Measure.infinitePi, with a pair joined when its coin falls below the graphon value — and its finite-marginal identification are formalized there. The construction is adapted to Tau Ceti's strict graphon carrier, whose values are everywhere in the unit interval, so no clamped representative is needed, and it lands on Mathlib's SimpleGraph ℕ with its adjacency sigma-algebra rather than on a Boolean cube of edge coordinates; the marginal proof here evaluates the mass of a single pattern as a box of coin intervals instead of going through upper events.

noncomputable def TauCeti.DenseGraphLimits.infiniteSampleLaw {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : MeasureTheory.Measure (SimpleGraph ℕ)

The joint sampling law of a graphon: the law of the infinite W-random graph on ℕ. All the finite sampling laws are windows of this single random object.

Equations

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

instance TauCeti.DenseGraphLimits.infiniteSampleLaw_isProbabilityMeasure {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : MeasureTheory.IsProbabilityMeasure (infiniteSampleLaw W)

@[simp]

theorem TauCeti.DenseGraphLimits.infiniteSampleLaw_map_restrictFin {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) (n : ℕ) : MeasureTheory.Measure.map (fun (G : SimpleGraph ℕ) => G.restrictFin n) (infiniteSampleLaw W) = sampleGraph W n

The finite marginals of the joint sampling law. The window of the infinite W-random graph spanned by the first n labels has the law of the W-random graph on Fin n: every finite sampling law is a restriction of this one random object.