Finite sampling from a graphon

The W-random graph on Fin n is obtained in two stages: first sample n independent points from the graphon's probability space, then include each unordered pair independently with probability given by the value of W at its two sampled points. This file integrates out both stages and packages the resulting masses as a probability measure on finite simple graphs.

The mass of a graph G is the integral of a finite product. Its edges contribute factors W, while its nonedges contribute factors 1 - W. At fixed vertex positions, summing this product over the graphs that decide a fixed set of pairs in a prescribed way expands as ∏ₑ (Wₑ + (1 - Wₑ)) = 1 over the remaining undecided pairs, leaving the factors of the decided ones. Requiring a fixed set of edges and leaving the rest free is the special case that computes the mass of an upper event, and deciding nothing at all gives normalization without imposing any extra regularity on the graphon's carrier.

Main definitions

• TauCeti.DenseGraphLimits.sampleIntegrand — the conditional mass of a graph at fixed sampled vertex positions;
• TauCeti.DenseGraphLimits.sampleMass — that mass after integrating over the positions;
• TauCeti.DenseGraphLimits.sampleGraph — the resulting probability measure.

Main results

• sum_sampleIntegrand_inter_eq computes the conditional mass of the graphs with a prescribed trace on a fixed set of pairs;
• sum_sampleIntegrand_superset_eq_prod_edgeFactor specializes it to the graphs containing a fixed set of edges;
• sampleIntegrand_eq_prod_edgeFinset_top writes the conditional mass as a single product over the pairs of the complete graph;
• sampleMass_nonneg and sum_sampleMass_eq_one show that the masses form a probability law;
• sampleGraph_singleton computes the probability of an individual graph;
• sampleGraph_const identifies sampling a constant graphon with Mathlib's binomial random graph.

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), Sections 10.1--10.2.
• C. Freer, cameronfreer/graphon at commit 6eccca5bbe5c9df46d7129bf59575b8b9b1d6699, Apache-2.0, Graphon/Sampling.lean, Graphon/SamplingLaw.lean, and Graphon/SamplingExamples.lean. The definitions and the Boolean-cube normalization argument, here generalized to a prescribed trace on a fixed set of pairs, are adapted to Tau Ceti's strict graphon carrier; the constant-law proof reuses the same reduction to Mathlib's singleton-mass formula.

noncomputable def TauCeti.DenseGraphLimits.sampleIntegrand {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) (G : SimpleGraph (Fin n)) (x : Fin n → Ω) : ℝ

The conditional mass of G at fixed sampled vertex positions. Edges contribute W and nonedges contribute 1 - W.

Equations

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

noncomputable def TauCeti.DenseGraphLimits.sampleMass {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) (G : SimpleGraph (Fin n)) : ℝ

The probability mass assigned to G by the W-random graph: integrate its conditional mass over the independently sampled vertex positions.

Equations

• TauCeti.DenseGraphLimits.sampleMass W G = ∫ (x : Fin n → Ω), TauCeti.DenseGraphLimits.sampleIntegrand W G x ∂MeasureTheory.Measure.pi fun (x : Fin n) => μ

theorem TauCeti.DenseGraphLimits.sampleIntegrand_def {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) (G : SimpleGraph (Fin n)) (x : Fin n → Ω) : sampleIntegrand W G x = (∏ e ∈ G.edgeFinset, edgeFactor W x e) * ∏ e ∈ ⊤.edgeFinset \ G.edgeFinset, (1 - edgeFactor W x e)

The defining edge/nonedge product of the sampled-graph integrand.

theorem TauCeti.DenseGraphLimits.sampleMass_def {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) (G : SimpleGraph (Fin n)) : sampleMass W G = ∫ (x : Fin n → Ω), sampleIntegrand W G x ∂MeasureTheory.Measure.pi fun (x : Fin n) => μ

The defining integral of a sampled graph's mass.

theorem TauCeti.DenseGraphLimits.measurable_sampleIntegrand {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) (G : SimpleGraph (Fin n)) : Measurable (sampleIntegrand W G)

The sampled-graph integrand is measurable in the vertex positions.

theorem TauCeti.DenseGraphLimits.sampleIntegrand_nonneg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) (G : SimpleGraph (Fin n)) (x : Fin n → Ω) : 0 ≤ sampleIntegrand W G x

The sampled-graph integrand is nonnegative.

theorem TauCeti.DenseGraphLimits.sampleIntegrand_le_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) (G : SimpleGraph (Fin n)) (x : Fin n → Ω) : sampleIntegrand W G x ≤ 1

The sampled-graph integrand is at most 1.

theorem TauCeti.DenseGraphLimits.integrable_sampleIntegrand {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) (G : SimpleGraph (Fin n)) : MeasureTheory.Integrable (sampleIntegrand W G) (MeasureTheory.Measure.pi fun (x : Fin n) => μ)

The sampled-graph integrand is integrable against the product probability measure.

theorem TauCeti.DenseGraphLimits.sampleIntegrand_eq_prod_edgeFinset_top {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) (G : SimpleGraph (Fin n)) (x : Fin n → Ω) : sampleIntegrand W G x = ∏ e ∈ ⊤.edgeFinset, if e ∈ G.edgeFinset then edgeFactor W x e else 1 - edgeFactor W x e

The conditional mass of G as a single product over the pairs of the complete graph: each pair contributes the graphon value if G joins it and the complementary value if it does not.

theorem TauCeti.DenseGraphLimits.sampleMass_nonneg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) (G : SimpleGraph (Fin n)) : 0 ≤ sampleMass W G

Sampled-graph masses are nonnegative.

theorem TauCeti.DenseGraphLimits.sampleMass_le_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) (G : SimpleGraph (Fin n)) : sampleMass W G ≤ 1

A sampled-graph mass is at most 1.

theorem TauCeti.DenseGraphLimits.sum_sampleIntegrand_inter_eq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) (A B : Finset (Sym2 (Fin n))) (hA : A ⊆ ⊤.edgeFinset) (hBA : B ⊆ A) (x : Fin n → Ω) : ∑ H : SimpleGraph (Fin n) with H.edgeFinset ∩ A = B, sampleIntegrand W H x = (∏ e ∈ B, edgeFactor W x e) * ∏ e ∈ A \ B, (1 - edgeFactor W x e)

At fixed vertex positions, summing the conditional masses over the graphs whose edges meet a fixed loop-free set A in a prescribed subset B collapses to the product of the edge factors of B against the complementary factors of A \ B: the edges left undecided by A contribute ∏ₑ (Wₑ + (1 - Wₑ)) = 1. Loop-freeness of A is expressed as containment in the edges of the complete graph.

theorem TauCeti.DenseGraphLimits.sum_sampleIntegrand_superset_eq_prod_edgeFactor {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) (T : Finset (Sym2 (Fin n))) (hT : T ⊆ ⊤.edgeFinset) (x : Fin n → Ω) : ∑ H : SimpleGraph (Fin n) with ↑T ⊆ H.edgeSet, sampleIntegrand W H x = ∏ e ∈ T, edgeFactor W x e

At fixed vertex positions, summing the conditional masses over every graph whose edges include a fixed loop-free set T collapses to the product of the edge factors of T: the optional edges outside T contribute ∏ₑ (Wₑ + (1 - Wₑ)) = 1. Loop-freeness of T is expressed as containment in the edges of the complete graph.

theorem TauCeti.DenseGraphLimits.sum_sampleIntegrand_eq_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) (x : Fin n → Ω) : ∑ H : SimpleGraph (Fin n), sampleIntegrand W H x = 1

At fixed vertex positions, the conditional masses sum to 1 over all simple graphs.

theorem TauCeti.DenseGraphLimits.sum_sampleMass_eq_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) : ∑ H : SimpleGraph (Fin n), sampleMass W H = 1

The sampled-graph masses sum to 1.

noncomputable def TauCeti.DenseGraphLimits.sampleGraph {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) (n : ℕ) : MeasureTheory.Measure (SimpleGraph (Fin n))

The W-random graph law on Fin n.

Equations

• TauCeti.DenseGraphLimits.sampleGraph W n = (TauCeti.DenseGraphLimits.samplePMF✝ W n).toMeasure

instance TauCeti.DenseGraphLimits.sampleGraph_isProbabilityMeasure {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) (n : ℕ) : MeasureTheory.IsProbabilityMeasure (sampleGraph W n)

A sampled graph law is a probability measure.

@[simp]

theorem TauCeti.DenseGraphLimits.sampleGraph_singleton {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) (n : ℕ) (G : SimpleGraph (Fin n)) : (sampleGraph W n) {G} = ENNReal.ofReal (sampleMass W G)

The probability that the sampled graph equals G.

@[simp]

theorem TauCeti.DenseGraphLimits.sampleMass_const {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (p : ↑unitInterval) (G : SimpleGraph (Fin n)) : sampleMass (Graphon.const μ p) G = ↑p ^ G.edgeFinset.card * (1 - ↑p) ^ (n.choose 2 - G.edgeFinset.card)

The sampled mass of a constant graphon is the usual independent-edge mass.

@[simp]

theorem TauCeti.DenseGraphLimits.sampleGraph_const {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (p : ↑unitInterval) (n : ℕ) : sampleGraph (Graphon.const μ p) n = SimpleGraph.binomialRandom (Fin n) p

Sampling a constant graphon gives Mathlib's binomial random graph law.