Exchangeable laws on infinite graphs

An exchangeable random graph on the labels ℕ is a probability law on SimpleGraph ℕ that is invariant under relabelling along every permutation of ℕ. Its windows — the laws of the restrictions to the labels Fin k — form an ExchangeableGraphLaw: restricting along an injection Fin k ↪ Fin l is, on the infinite graph, relabelling by a permutation of ℕ extending the injection, followed by taking the smaller window. Conversely every ExchangeableGraphLaw is the family of windows of exactly one such law, so the two presentations of an exchangeable random graph agree (exchangeableGraphLawEquivInfinite).

Uniqueness holds because a finite measure on SimpleGraph ℕ is determined by its windows (measure_ext_of_map_restrictFin). Existence is Kolmogorov's extension theorem: reading an infinite graph through its Boolean edge coordinates graphCoordEquiv, the level-n marginals prescribe a projective family of laws on the finitely many coordinates below any bound, and a projective limit on the countable product of the coordinates exists. The extension is exchangeable because each window of a relabelled extension is a restriction of a larger window along an injection, which the consistency of the marginals controls.

Main definitions

• TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw — a relabelling-invariant probability law on the graphs on ℕ;
• TauCeti.DenseGraphLimits.exchangeableGraphLawEquivInfinite — consistent finite marginals are the same thing as an exchangeable law on infinite graphs.

Main results

• TauCeti.DenseGraphLimits.exchangeableGraphLawEquivInfinite_law_map_restrictFin — the windows of the infinite law attached to an exchangeable graph law are its marginals;
• TauCeti.DenseGraphLimits.exchangeableGraphLawEquivInfinite_symm_law — conversely the marginals attached to an infinite law are its windows.

References

• P. Diaconis, S. Janson, Graph limits and exchangeable random graphs, Rend. Mat. Appl. (7) 28 (2008), 33--61, Section 5.
• C. Freer, cameronfreer/graphon at commit 6eccca5bbe5c9df46d7129bf59575b8b9b1d6699, Apache-2.0, Graphon/InfiniteLaw.lean and Graphon/InfiniteExchangeability.lean, a prior formalization of the same equivalence between consistent marginals and exchangeable laws on infinite graphs.

The extension of consistent marginals

Exchangeable laws on infinite graphs

structure TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw : Type

An exchangeable law on infinite graphs: a probability law on the graphs on ℕ invariant under relabelling along every permutation of ℕ.

• law : MeasureTheory.Measure (SimpleGraph ℕ)

  The law on infinite graphs.

• prob : MeasureTheory.IsProbabilityMeasure self.law

  It is a probability measure.

• exchangeable (σ : Equiv.Perm ℕ) : MeasureTheory.Measure.map (SimpleGraph.comap ⇑σ) self.law = self.law

  Invariance under every relabelling.

instance TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.instIsProbabilityMeasureLaw (L : InfiniteExchangeableGraphLaw) : MeasureTheory.IsProbabilityMeasure L.law

theorem TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.ext {L L' : InfiniteExchangeableGraphLaw} (h : L.law = L'.law) : L = L'

An exchangeable law on infinite graphs is determined by its law: the other fields are propositions.

theorem TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.ext_iff {L L' : InfiniteExchangeableGraphLaw} : L = L' ↔ L.law = L'.law

noncomputable def TauCeti.DenseGraphLimits.exchangeableGraphLawEquivInfinite : ExchangeableGraphLaw ≃ InfiniteExchangeableGraphLaw

Consistent finite marginals are an exchangeable law on infinite graphs. An exchangeable graph law extends to a unique relabelling-invariant law on the graphs on ℕ whose windows are its marginals; conversely the windows of such a law are consistent marginals.

Equations

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

@[simp]

theorem TauCeti.DenseGraphLimits.exchangeableGraphLawEquivInfinite_law_map_restrictFin (L : ExchangeableGraphLaw) (k : ℕ) : MeasureTheory.Measure.map (fun (x : SimpleGraph ℕ) => x.restrictFin k) (exchangeableGraphLawEquivInfinite L).law = L.law k

The windows of the extension are the marginals. The level-k window of the infinite law attached to an exchangeable graph law is its level-k marginal.

@[simp]

theorem TauCeti.DenseGraphLimits.exchangeableGraphLawEquivInfinite_symm_law (L : InfiniteExchangeableGraphLaw) (k : ℕ) : (exchangeableGraphLawEquivInfinite.symm L).law k = MeasureTheory.Measure.map (fun (x : SimpleGraph ℕ) => x.restrictFin k) L.law

The marginals attached to an exchangeable law on infinite graphs are its windows.

theorem TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.map_comap_restrictFin (L : InfiniteExchangeableGraphLaw) {k l : ℕ} (f : Fin l ↪ Fin k) : MeasureTheory.Measure.map (fun (G : SimpleGraph ℕ) => SimpleGraph.comap (⇑f) (G.restrictFin k)) L.law = MeasureTheory.Measure.map (fun (x : SimpleGraph ℕ) => x.restrictFin l) L.law

A window read along an embedding of labels has the law of the window of its length.

theorem TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.map_comap_natAdd_restrictFin (L : InfiniteExchangeableGraphLaw) (k l : ℕ) : MeasureTheory.Measure.map (fun (G : SimpleGraph ℕ) => SimpleGraph.comap (Fin.natAdd k) (G.restrictFin (k + l))) L.law = MeasureTheory.Measure.map (fun (x : SimpleGraph ℕ) => x.restrictFin l) L.law

The second of two consecutive windows has the law of the window of its length.