The explicit infinite sampler for a fixed graphon (issue #51, sources + sampler)

Reusable i.i.d. product sources via Measure.infinitePi, and the explicit measurable sampler from those sources to the infinite graph space:

• InfiniteGraph.vertexSource — i.i.d. vertex positions ℕ → α with law μ;

• InfiniteGraph.edgeSource — i.i.d. edge uniforms on [0,1], indexed by EdgeIndex;

• InfiniteGraph.clampedRep W — the everywhere-[0,1]-valued clamped representative of the graphon (a.e. equal to it);

• InfiniteGraph.sampleInfinite W — one uniform per unordered edge, compared against the clamped graphon value at the Quot.out-representative endpoint positions (matching sampleIntegrand's orientation): measurable in the sources.

• InfiniteGraph.map_sampleInfinite_restrictFin — the finite marginal identification: the sampler's level-k law is exactly samplePMF W k (upper-event route: F ≤ G needs only the edges of F, so conditional edge integration produces the plain W-product; upperSum_injective closes);

• InfiniteGraph.map_sampleInfinite — the explicit realization theorem: the sampler's law is infiniteLaw (sampleExchangeableLaw W) (A2 uniqueness), with relabeling invariance (map_sampleInfinite_relabel) and the canonical-class form (map_sampleInfinite_eq_infiniteSampleLaw_mk) as corollaries.

noncomputable def InfiniteGraph.uniform01 : MeasureTheory.Measure ℝ

The uniform distribution on [0,1].

Equations

• InfiniteGraph.uniform01 = MeasureTheory.volume.restrict (Set.Icc 0 1)

instance InfiniteGraph.instIsProbabilityMeasureRealUniform01 : MeasureTheory.IsProbabilityMeasure uniform01

noncomputable def InfiniteGraph.vertexSource {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) : MeasureTheory.Measure (ℕ → α)

The vertex source: i.i.d. positions ℕ → α with law μ.

Equations

• InfiniteGraph.vertexSource μ = MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ

noncomputable def InfiniteGraph.edgeSource : MeasureTheory.Measure (EdgeIndex → ℝ)

The edge source: i.i.d. uniforms on [0,1], one per unordered edge.

Equations

• InfiniteGraph.edgeSource = MeasureTheory.Measure.infinitePi fun (x : InfiniteGraph.EdgeIndex) => InfiniteGraph.uniform01

instance InfiniteGraph.instIsProbabilityMeasureForallNatVertexSource {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.IsProbabilityMeasure (vertexSource μ)

instance InfiniteGraph.instIsProbabilityMeasureForallEdgeIndexRealEdgeSource : MeasureTheory.IsProbabilityMeasure edgeSource

noncomputable def InfiniteGraph.samplerSource {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) : MeasureTheory.Measure ((ℕ → α) × (EdgeIndex → ℝ))

The sampler source: independent vertex positions and edge uniforms.

Equations

• InfiniteGraph.samplerSource μ = (InfiniteGraph.vertexSource μ).prod InfiniteGraph.edgeSource

instance InfiniteGraph.instIsProbabilityMeasureProdForallNatForallEdgeIndexRealSamplerSource {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.IsProbabilityMeasure (samplerSource μ)

noncomputable def InfiniteGraph.clampedRep {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) (p : α × α) : ℝ

The clamped [0,1]-valued representative of a graphon: an everywhere-valid edge probability (the graphon is only a.e. [0,1]-valued; clamping isolates the eventual a.e.-congruence argument).

Equations

• InfiniteGraph.clampedRep W p = min 1 (max 0 (↑W.toAEEqFun p))

theorem InfiniteGraph.clampedRep_mem_Icc {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) (p : α × α) : clampedRep W p ∈ Set.Icc 0 1

theorem InfiniteGraph.measurable_clampedRep {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) : Measurable (clampedRep W)

theorem InfiniteGraph.clampedRep_ae_eq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) : ∀ᵐ (p : α × α) ∂μ.prod μ, clampedRep W p = ↑W.toAEEqFun p

The clamped representative agrees with the graphon almost everywhere.

noncomputable def InfiniteGraph.sampleInfinite {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) (ω : (ℕ → α) × (EdgeIndex → ℝ)) : InfiniteGraph

The explicit infinite sampler: include the edge e exactly when its uniform falls below the clamped graphon value at the Quot.out-representative endpoint positions (matching the orientation convention of sampleIntegrand, which eliminates the a.e.-symmetry orientation juggling in the marginal identification).

Equations

• One or more equations did not get rendered due to their size.

theorem InfiniteGraph.coordEquiv_sampleInfinite {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) (ω : (ℕ → α) × (EdgeIndex → ℝ)) (e : EdgeIndex) : coordEquiv (sampleInfinite W ω) e = if ω.2 e ≤ clampedRep W (ω.1 (Quot.out ↑e).1, ω.1 (Quot.out ↑e).2) then true else false

The edge coordinates of a sample, unfolded.

theorem InfiniteGraph.measurable_sampleInfinite {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) : Measurable (sampleInfinite W)

The sampler is measurable in the sources: each edge coordinate is a measurable comparison.

The finite marginal identification (issue #51, brick 2)

restrictFin k ∘ sampleInfinite W pushes the sampler source forward to exactly the finite sample law samplePMF W k, and hence sampleInfinite W realizes the infinite exchangeable law of sampleExchangeableLaw W. Route: reduce singleton masses to upper events {G | F ≤ G} via Möbius inversion (upperSum_injective); the upper event is a finite cylinder over the (injectively indexed) edge uniforms, whose vertex-conditional probability is the clamped edge product; integrating out the positions gives homDensity F W, which is also the upper transform of sampleMass W.

theorem InfiniteGraph.vertexSource_map_fin {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (k : ℕ) : MeasureTheory.Measure.map (fun (x : ℕ → α) (a : Fin k) => x ↑a) (vertexSource μ) = MeasureTheory.Measure.pi fun (x : Fin k) => μ

The joint law of the first k vertex positions is the finite i.i.d. product.

theorem InfiniteGraph.map_sampleInfinite_restrictFin {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) [MeasureTheory.IsProbabilityMeasure μ] (k : ℕ) : MeasureTheory.Measure.map (restrictFin k ∘ sampleInfinite W) (samplerSource μ) = (W.samplePMF k).toMeasure

The finite marginal identification (issue #51, brick 2): the law of the first- k-vertices restriction of the sampled infinite graph is exactly the finite sample law samplePMF W k.

theorem InfiniteGraph.map_sampleInfinite {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.Measure.map (sampleInfinite W) (samplerSource μ) = ↑W.sampleExchangeableLaw.infiniteLaw

The sampler realizes the infinite exchangeable law (issue #51): the pushforward of the sampler source under sampleInfinite W is the (A2-unique) infinite law of the sample exchangeable law of W.

theorem InfiniteGraph.map_sampleInfinite_relabel {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) [MeasureTheory.IsProbabilityMeasure μ] (σ : Equiv.Perm ℕ) : MeasureTheory.Measure.map (relabel σ) (MeasureTheory.Measure.map (sampleInfinite W) (samplerSource μ)) = MeasureTheory.Measure.map (sampleInfinite W) (samplerSource μ)

Exchangeability of the sampler's law: free from map_sampleInfinite, since the infinite law is invariant under every relabeling of ℕ.

theorem InfiniteGraph.map_sampleInfinite_eq_infiniteSampleLaw_mk {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) : MeasureTheory.Measure.map (sampleInfinite W) (samplerSource μ) = ↑(GraphonSpace.mk W).infiniteSampleLaw

The canonical-class form of the realization theorem: the sampler's law is the canonical infinite law of the graphon class of W.