The universal measurable empirical limit (issue #58)

One measure-independent limit function for the empirical graphons of an infinite graph, stated at the canonical instance (α := unitInterval, μ := volume, codomain StandardGraphonSpace):

• GraphonSpace.empiricalConvergenceSet — the (measurable, measure-independent) set of infinite graphs whose empirical graphons converge in the standard graphon space (measurableSet_empiricalConvergenceSet, via MeasureTheory.measurableSet_exists_tendsto);
• GraphonSpace.limitGraphon — the universal empirical limit: the unique limit on the convergence set, the explicit zero-graphon class off it; measurable everywhere (measurable_limitGraphon: metrizable-limit measurability on the convergence-set subtype, glued with the constant on the measurable complement);
• GraphonSpace.ae_tendsto_empiricalGraphon_infiniteSampleLaw — the per-class fiber theorem: under the canonical infinite law of EVERY class x, the empirical graphons converge to x almost surely (the almost-sure sampling theorem of issue #71, transported along the explicit-sampler realization of issue #51);
• under any infinite exchangeable law M, the convergence set is conull (ae_mem_empiricalConvergenceSet, via the barycenter identification of issue #54) and the empirical graphons converge to limitGraphon almost surely (ae_tendsto_empiricalGraphon_limitGraphon);
• GraphonSpace.map_limitGraphon_law — the distributional identification: the law of limitGraphon under M is exactly the representing mixing measure infiniteMixtureLawEquiv.symm M — the empirical limit realizes the mixture coordinate as a genuine random variable.

Pointwise finite-permutation invariance of limitGraphon is deferred to issue #59: it needs isomorphism-invariance of the finite graph classes (graphClass ∘ comap by a Fin-permutation), which is not yet in the library.

def GraphonSpace.empiricalConvergenceSet : Set InfiniteGraph

The empirical convergence set: the infinite graphs whose empirical graphons converge in the standard graphon space. Measure-independent — the domain of the universal empirical limit limitGraphon.

Equations

• GraphonSpace.empiricalConvergenceSet = {G : InfiniteGraph | ∃ (x : StandardGraphonSpace), Filter.Tendsto (fun (n : ℕ) => GraphonSpace.empiricalGraphon n G) Filter.atTop (nhds x)}

theorem GraphonSpace.measurableSet_empiricalConvergenceSet : MeasurableSet empiricalConvergenceSet

The empirical convergence set is measurable (the codomain is completely metrizable and second countable).

noncomputable def GraphonSpace.limitGraphon (G : InfiniteGraph) : StandardGraphonSpace

The universal empirical limit: the limit of the empirical graphons on the convergence set, the class of the zero graphon (the explicit canonical default, not an arbitrary inhabitant) off it. Measure-independent — one function for all exchangeable laws at once.

Equations

• GraphonSpace.limitGraphon G = if h : G ∈ GraphonSpace.empiricalConvergenceSet then Exists.choose h else GraphonSpace.mk (Graphon.constGraphon 0)

theorem GraphonSpace.limitGraphon_eq_of_tendsto {G : InfiniteGraph} {x : StandardGraphonSpace} (h : Filter.Tendsto (fun (n : ℕ) => empiricalGraphon n G) Filter.atTop (nhds x)) : limitGraphon G = x

The universal empirical limit computes any actual limit (limits are unique in the Hausdorff graphon space).

theorem GraphonSpace.measurable_limitGraphon : Measurable limitGraphon

The universal empirical limit is measurable: on the convergence-set subtype it is a pointwise limit of measurable functions into a metrizable space; on the measurable complement it is constant.

theorem GraphonSpace.ae_tendsto_empiricalGraphon_infiniteSampleLaw (x : StandardGraphonSpace) : ∀ᵐ (G : InfiniteGraph) ∂↑(infiniteSampleLaw x), Filter.Tendsto (fun (n : ℕ) => empiricalGraphon n G) Filter.atTop (nhds x)

The per-class fiber theorem (every class, not just almost every): under the canonical infinite law of ANY graphon class x, the empirical graphons converge to x almost surely — the almost-sure sampling theorem (issue #71) transported along the explicit-sampler realization (issue #51) of the fiber law.

theorem GraphonSpace.law_eq_bind_infiniteSampleLaw (M : Graphon.InfiniteExchangeableGraphLaw) : ↑M.law = (↑(infiniteMixtureLawEquiv.symm M)).bind fun (x : GraphonSpace (↑unitInterval) MeasureTheory.volume) => ↑x.infiniteSampleLaw

The barycenter form of an infinite exchangeable law at the canonical instance: M.law is the mixture of the canonical fiber laws over the representing mixing measure infiniteMixtureLawEquiv.symm M (the coerced form of the barycenter identification mixtureInfiniteLaw_eq of issue #54).

theorem GraphonSpace.ae_mem_empiricalConvergenceSet (M : Graphon.InfiniteExchangeableGraphLaw) : ∀ᵐ (G : InfiniteGraph) ∂↑M.law, G ∈ empiricalConvergenceSet

The convergence set is conull under every infinite exchangeable law: by the barycenter identification, its complement has zero mass in every fiber (the per-class fiber theorem), hence zero mass in the mixture.

theorem GraphonSpace.ae_tendsto_empiricalGraphon_limitGraphon (M : Graphon.InfiniteExchangeableGraphLaw) : ∀ᵐ (G : InfiniteGraph) ∂↑M.law, Filter.Tendsto (fun (n : ℕ) => empiricalGraphon n G) Filter.atTop (nhds (limitGraphon G))

Almost-sure convergence to the universal limit: under every infinite exchangeable law, the empirical graphons converge to limitGraphon almost surely.

theorem GraphonSpace.map_limitGraphon_law (M : Graphon.InfiniteExchangeableGraphLaw) : M.law.map ⋯ = infiniteMixtureLawEquiv.symm M

The distributional identification (issue #58): under any infinite exchangeable law M, the law of the universal empirical limit is exactly the representing mixing measure infiniteMixtureLawEquiv.symm M. Fiberwise, the limit is almost surely the fiber point, so each fiber gives the preimage of a measurable set indicator mass; the barycenter integrates the indicator back to the mixing measure.

theorem GraphonSpace.map_limitGraphon_law_coe (M : Graphon.InfiniteExchangeableGraphLaw) : MeasureTheory.Measure.map limitGraphon ↑M.law = ↑(infiniteMixtureLawEquiv.symm M)

The distributional identification, as an equality of raw pushforward measures.