Consistency of graphon sampling under restriction of labels

Sampling l independent points from a graphon and then tossing an independent coin for each unordered pair produces a law on SimpleGraph (Fin l). Restricting such a sample to a window of k labels is the same as running the k-point sampling procedure from the start: the window reads k of the l independent points, which are again independent with the same law, and the coins outside the window are simply not looked at.

The combinatorial half is that the graphs on Fin l restricting to a fixed H along an injection f are exactly the graphs whose edges meet the window ⊤.map f in the image of the edges of H. Summing the conditional masses over that family collapses the coins outside the window, leaving the conditional mass of H at the restricted positions. The probabilistic half is that restricting an independent family of positions along an injection is measure preserving.

Main results

• TauCeti.DenseGraphLimits.sum_sampleIntegrand_comap_eq — at fixed positions, the conditional masses of the graphs restricting to H sum to the conditional mass of H at the restricted positions;
• TauCeti.DenseGraphLimits.sum_sampleMass_comap_eq — the same identity after integrating out the positions;
• TauCeti.DenseGraphLimits.sampleGraph_map_comap — the sampling laws are consistent under restriction along every injection of labels.

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), Section 10.1.
• P. Diaconis, S. Janson, Graph limits and exchangeable random graphs, Rend. Mat. Appl. (7) 28 (2008), 33--61, Section 5.
• C. Freer, cameronfreer/graphon at commit 6eccca5bbe5c9df46d7129bf59575b8b9b1d6699, Apache-2.0, Graphon/ExchangeableGraphLaw.lean. The consistency statement follows that source; the proof here is written for Tau Ceti's strict graphon carrier and reduces the combinatorial step to the prescribed-trace mass formula.

theorem TauCeti.DenseGraphLimits.sum_sampleIntegrand_comap_eq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {k l : ℕ} (W : Graphon Ω μ) (f : Fin k ↪ Fin l) (H : SimpleGraph (Fin k)) (x : Fin l → Ω) : ∑ G : SimpleGraph (Fin l) with SimpleGraph.comap (⇑f) G = H, sampleIntegrand W G x = sampleIntegrand W H (x ∘ ⇑f)

At fixed vertex positions, the conditional masses of the graphs restricting to H along f sum to the conditional mass of H at the restricted positions: such a graph is prescribed on the window seen by f and free outside it, and the free coins contribute 1.

theorem TauCeti.DenseGraphLimits.sum_sampleMass_comap_eq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {k l : ℕ} (W : Graphon Ω μ) (f : Fin k ↪ Fin l) (H : SimpleGraph (Fin k)) : ∑ G : SimpleGraph (Fin l) with SimpleGraph.comap (⇑f) G = H, sampleMass W G = sampleMass W H

The masses of the graphs restricting to H along f sum to the mass of H: integrating the conditional identity over the positions, which the restriction to the window redistributes without changing their law.

@[simp]

theorem TauCeti.DenseGraphLimits.sampleGraph_map_comap {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {k l : ℕ} (W : Graphon Ω μ) (f : Fin k ↪ Fin l) : MeasureTheory.Measure.map (SimpleGraph.comap ⇑f) (sampleGraph W l) = sampleGraph W k

Consistency of graphon sampling. Restricting a sample on Fin l to a window of k labels has the law of a sample on Fin k.