Convergence in measure of graphon samples

The finite sampling laws of a graphon are the marginals of one infinite random graph. Applying the finite-graph graphon construction to its growing windows gives a sequence of points in the unit-interval cut-distance quotient GraphonSpaceI. The second sampling lemma says that this sequence converges in measure to the original graphon's class. The generating graphon may live on any probability carrier: its class is taken in GraphonSpaceI through the isometric embedding toGraphonSpaceI. The joint-law formulation allows the same random graph to be used at every window size.

Main results

• TauCeti.DenseGraphLimits.infiniteSampleLaw_tendstoInMeasure_toGraphonSpaceI packages the second sampling lemma on the joint probability space, for a graphon on any probability carrier.
• TauCeti.DenseGraphLimits.infiniteSampleLaw_tendstoInMeasure_cutDist is its specialization to graphons on the unit interval.

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), Lemma 10.16.

theorem TauCeti.DenseGraphLimits.infiniteSampleLaw_tendstoInMeasure_toGraphonSpaceI {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : MeasureTheory.TendstoInMeasure (infiniteSampleLaw W) (fun (n : ℕ) (G : SimpleGraph ℕ) => SeparationQuotient.mk (finiteGraphGraphon (G.restrictFin (n + 1)))) Filter.atTop fun (x : SimpleGraph ℕ) => toGraphonSpaceI (SeparationQuotient.mk W)

Under the joint sampling law of a graphon W on any probability carrier, the graphon classes of the finite windows converge in measure, in GraphonSpaceI, to the image of the class of W under the isometric embedding toGraphonSpaceI. The window has n + 1 vertices, so the construction also covers the first term without a nonempty-carrier convention.

theorem TauCeti.DenseGraphLimits.infiniteSampleLaw_tendstoInMeasure_cutDist (W : Graphon (↑unitInterval) MeasureTheory.volume) : MeasureTheory.TendstoInMeasure (infiniteSampleLaw W) (fun (n : ℕ) (G : SimpleGraph ℕ) => SeparationQuotient.mk (finiteGraphGraphon (G.restrictFin (n + 1)))) Filter.atTop fun (x : SimpleGraph ℕ) => SeparationQuotient.mk W

Under the joint sampling law of a unit-interval graphon, the graphon classes of the finite windows converge in measure to the class of the generating graphon.