Exchangeable graph laws and graphon mixtures (issue #33, foundations)

An exchangeable (infinite) random graph is presented by its consistent finite marginals — the form in which the Diaconis–Janson content is cleanest. (Historically this also side-stepped laws on SimpleGraph ℕ while no extension theorem was available; the equivalent infinite formulation now exists — Graphon/InfiniteLaw.lean constructs the unique extension by compactness, and Graphon/InfiniteExchangeability.lean packages ExchangeableGraphLaw ≃ InfiniteExchangeableGraphLaw.)

• Graphon.ExchangeableGraphLaw — a family law k : PMF (SimpleGraph (Fin k)) consistent under every injection of labels (which subsumes relabeling invariance);
• Graphon.sampleExchangeableLaw — the sample laws of a fixed graphon form an exchangeable graph law (samplePMF_map_comap);
• GraphonSpace.mixturePMF — the k-vertex marginal of a graphon mixture: the sample-law masses integrated against a probability measure on the graphon space;
• GraphonSpace.mixturePMF_dirac — a Dirac mixture recovers the sample law of the underlying graphon class;
• GraphonSpace.mixtureExchangeableLaw — every graphon mixture is exchangeable (mixturePMF_map_comap).

The Diaconis–Janson correspondence (issue #33) states the converse: every exchangeable graph law is a unique graphon mixture. This file provides its objects and the easy direction; the representation theorem itself is the campaign target.

structure Graphon.ExchangeableGraphLaw : Type

An exchangeable graph law, presented by its consistent finite marginals: a k-vertex law for every k, consistent under restriction along every injection of labels. Arbitrary-injection consistency subsumes relabeling invariance (permutations are injections).

• law (k : ℕ) : PMF (SimpleGraph (Fin k))

  The k-vertex marginal.

• consistent {k l : ℕ} (e : Fin k ↪ Fin l) : PMF.map (fun (G : SimpleGraph (Fin l)) => SimpleGraph.comap (⇑e) G) (self.law l) = self.law k

  Consistency under restriction along every injection of labels.

theorem Graphon.ExchangeableGraphLaw.ext {L M : ExchangeableGraphLaw} (h : ∀ (k : ℕ), L.law k = M.law k) : L = M

theorem Graphon.ExchangeableGraphLaw.ext_iff {L M : ExchangeableGraphLaw} : L = M ↔ ∀ (k : ℕ), L.law k = M.law k

noncomputable def Graphon.sampleExchangeableLaw {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) : ExchangeableGraphLaw

The sample laws of a fixed graphon form an exchangeable graph law.

Equations

• W.sampleExchangeableLaw = { law := fun (k : ℕ) => W.samplePMF k, consistent := ⋯ }

@[simp]

theorem Graphon.sampleExchangeableLaw_law {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (k : ℕ) : W.sampleExchangeableLaw.law k = W.samplePMF k

theorem GraphonSpace.measurable_finiteSampleLaw_apply {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (k : ℕ) (G : SimpleGraph (Fin k)) : Measurable fun (x : GraphonSpace α μ) => (finiteSampleLaw k x) G

Each ENNReal-valued mass coordinate is measurable on the graphon space.

noncomputable def GraphonSpace.mixturePMF {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)) (k : ℕ) : PMF (SimpleGraph (Fin k))

The k-vertex marginal of a graphon mixture: sample a graphon class from P, then sample the k-vertex graph from it. The mass of G is the integral of the sample-law masses against P.

Equations

• GraphonSpace.mixturePMF P k = PMF.ofFintype (fun (G : SimpleGraph (Fin k)) => ∫⁻ (x : GraphonSpace α μ), (GraphonSpace.finiteSampleLaw k x) G ∂↑P) ⋯

@[simp]

theorem GraphonSpace.mixturePMF_apply {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)) (k : ℕ) (G : SimpleGraph (Fin k)) : (mixturePMF P k) G = ∫⁻ (x : GraphonSpace α μ), (finiteSampleLaw k x) G ∂↑P

@[simp]

theorem GraphonSpace.mixturePMF_dirac {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (x : GraphonSpace α μ) (k : ℕ) : mixturePMF ⟨MeasureTheory.Measure.dirac x, ⋯⟩ k = finiteSampleLaw k x

A Dirac mixture recovers the sample law of the underlying graphon class.

theorem GraphonSpace.mixturePMF_apply_toReal {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)) (k : ℕ) (G : SimpleGraph (Fin k)) : ((mixturePMF P k) G).toReal = ∫ (x : GraphonSpace α μ), sampleMassCoord G x ∂↑P

The mixture marginal masses are Bochner integrals of the scalar coordinates sampleMassCoord.

theorem GraphonSpace.continuous_mixturePMF_apply_toReal {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (k : ℕ) (G : SimpleGraph (Fin k)) : Continuous fun (P : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)) => ((mixturePMF P k) G).toReal

The mixture coordinates are weakly continuous in the mixing measure: the exact interface for identifying Prokhorov limits (marginals of a weak limit are the limits of the marginals).

theorem GraphonSpace.mixturePMF_map_comap {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)) {k l : ℕ} (e : Fin k ↪ Fin l) : PMF.map (fun (G : SimpleGraph (Fin l)) => SimpleGraph.comap (⇑e) G) (mixturePMF P l) = mixturePMF P k

Graphon mixtures are exchangeable: the mixture marginals are consistent under every injection of labels.

noncomputable def GraphonSpace.mixtureExchangeableLaw {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)) : Graphon.ExchangeableGraphLaw

Every graphon mixture is an exchangeable graph law — the easy direction of the Diaconis–Janson correspondence (issue #33: the representation theorem states that this map from mixtures to exchangeable laws is a bijection).

Equations

• GraphonSpace.mixtureExchangeableLaw P = { law := fun (k : ℕ) => GraphonSpace.mixturePMF P k, consistent := ⋯ }

@[simp]

theorem GraphonSpace.mixtureExchangeableLaw_law {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)) (k : ℕ) : (mixtureExchangeableLaw P).law k = mixturePMF P k