Convergence in probability for the fixed-graphon sampler (issue #57, part 1)

The empirical graphons of an explicit W-random infinite graph converge to the class of W in probability:

• InfiniteGraph.sampledEmpiricalGraphon W n ω — the empirical graphon of the sampled infinite graph at level n + 1 (measurable in the sources);
• InfiniteGraph.sampledEmpiricalGraphon_tendstoInMeasure — convergence in probability: for every ε > 0 the probability that the empirical graphon is ε-far from mk W tends to 0. The bad event is the pullback of the complement of the sampleGoodMassOn event; its measure is 1 − sampleGoodMassOn W (n+1) ε by the marginal identification, and the project's first_sampling_lemma_of_large_k (the manuscript's Second Sampling Lemma, Lovász Lemma 10.16 — see the crosswalk in issue #18) drives it to zero.

The almost-sure strengthening (issue #71, the manuscript's Proposition 11.32) is proved in Graphon/AlmostSureSampling.lean, via the exponential hom-density concentration of Graphon/SampleExposure.lean and Borel–Cantelli.

noncomputable def InfiniteGraph.sampledEmpiricalGraphon {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (n : ℕ) (ω : (ℕ → α) × (EdgeIndex → ℝ)) : GraphonSpace α μ

The sampled empirical graphon at level n + 1: sample a W-random infinite graph, restrict to the first n + 1 vertices, take its graphon class.

Equations

• InfiniteGraph.sampledEmpiricalGraphon W n ω = GraphonSpace.empiricalGraphon n (InfiniteGraph.sampleInfinite W ω)

theorem InfiniteGraph.measurable_sampledEmpiricalGraphon {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (n : ℕ) : Measurable (sampledEmpiricalGraphon W n)

theorem InfiniteGraph.sampledEmpiricalGraphon_tendstoInMeasure {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) : MeasureTheory.TendstoInMeasure (samplerSource μ) (sampledEmpiricalGraphon W) Filter.atTop fun (x : (ℕ → α) × (EdgeIndex → ℝ)) => GraphonSpace.mk W

Convergence in probability of the sampled empirical graphons (issue #57, part 1): the empirical graphons of a W-random infinite graph tend to the class of W in measure.