The canonical infinite law of a graphon class (issue #52)

The infinite exchangeable law descends to graphon space, abstractly — no explicit sampler required (issue #51 later supplies a raw realization):

• GraphonSpace.infiniteSampleLaw — the canonical law of a graphon class on the infinite graph space, descended through the quotient (well-defined by the joining theorem);
• GraphonSpace.infiniteSampleLaw_mk — on classes, it is the infinite extension of the fixed-graphon sample law;
• GraphonSpace.infiniteSampleLaw_map_restrictFin — its finite restrictions are the finite sample laws;
• GraphonSpace.continuous_infiniteSampleLaw — weak continuity, by subsequential extraction and marginal identification (compactness + uniqueness);
• GraphonSpace.injective_infiniteSampleLaw and GraphonSpace.isClosedEmbedding_infiniteSampleLaw — the graphon space embeds as a compact set of probability laws on InfiniteGraph.

This removes representatives from all subsequent law-level arguments.

noncomputable def GraphonSpace.infiniteSampleLaw {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : GraphonSpace α μ → MeasureTheory.ProbabilityMeasure InfiniteGraph

The canonical infinite law of a graphon class: the infinite extension of the sample laws, descended through the quotient (well-defined by the joining theorem).

Equations

• GraphonSpace.infiniteSampleLaw = SeparationQuotient.lift (fun (W : Graphon α μ) => W.sampleExchangeableLaw.infiniteLaw) ⋯

@[simp]

theorem GraphonSpace.infiniteSampleLaw_mk {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) : (mk W).infiniteSampleLaw = W.sampleExchangeableLaw.infiniteLaw

theorem GraphonSpace.infiniteSampleLaw_map_restrictFin {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (x : GraphonSpace α μ) (k : ℕ) : MeasureTheory.Measure.map (InfiniteGraph.restrictFin k) ↑x.infiniteSampleLaw = (finiteSampleLaw k x).toMeasure

The finite restrictions of the canonical infinite law are the finite sample laws.

theorem GraphonSpace.continuous_infiniteSampleLaw {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : Continuous infiniteSampleLaw

Weak continuity of the canonical infinite law: subsequential Prokhorov extraction plus marginal identification (compactness and uniqueness).

theorem GraphonSpace.injective_infiniteSampleLaw {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : Function.Injective infiniteSampleLaw

Injectivity: the canonical infinite law determines the graphon class (finite restrictions recover the sample laws, which separate points).

theorem GraphonSpace.isClosedEmbedding_infiniteSampleLaw {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : Topology.IsClosedEmbedding infiniteSampleLaw

The graphon space embeds as a compact set of probability laws on InfiniteGraph: continuous injection from a compact space into a Hausdorff space (the infinite analogue of the finite coordinate embedding isClosedEmbedding_sampleCoordinates; the image consists of exchangeable laws, but the codomain is ProbabilityMeasure InfiniteGraph).