Empirical graphons of an infinite exchangeable graph (issue #56)

Cashing out the empirical convergence theorem at the infinite level:

• GraphonSpace.empiricalGraphon n G — the graphon class of the first n + 1 vertices of an infinite graph (successor indexing discharges NeZero);
• GraphonSpace.map_empiricalGraphon — its law under an infinite exchangeable law M is exactly the empirical mixing measure of M's finite marginals;
• GraphonSpace.empiricalGraphon_law_tendsto — the laws of the empirical graphons converge weakly to the representing measure infiniteMixtureLawEquiv.symm M (immediate from empiricalMixing_tendsto_representingMeasure).

noncomputable def GraphonSpace.empiricalGraphon {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (n : ℕ) (G : InfiniteGraph) : GraphonSpace α μ

The empirical graphon at level n + 1: the graphon class of the restriction of an infinite graph to its first n + 1 vertices.

Equations

• GraphonSpace.empiricalGraphon n G = GraphonSpace.graphClass (InfiniteGraph.restrictFin (n + 1) G)

theorem GraphonSpace.measurable_empiricalGraphon {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (n : ℕ) : Measurable (empiricalGraphon n)

@[simp]

theorem GraphonSpace.map_empiricalGraphon {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (M : Graphon.InfiniteExchangeableGraphLaw) (n : ℕ) : MeasureTheory.Measure.map (empiricalGraphon n) ↑M.law = ↑(empiricalMixing M.toExchangeableGraphLaw (n + 1))

The law of the empirical graphon is the empirical mixing measure of the finite marginals.

theorem GraphonSpace.empiricalGraphon_law_tendsto {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (M : Graphon.InfiniteExchangeableGraphLaw) : Filter.Tendsto (fun (n : ℕ) => M.law.map ⋯) Filter.atTop (nhds (infiniteMixtureLawEquiv.symm M))

Empirical graphons converge in distribution to the representing measure: the distributional cash-out of the empirical convergence theorem at the infinite level.