Exchangeability of the infinite law, and the packaged equivalence (brick A3)

The infinite law of an exchangeable graph law is invariant under every relabeling of ℕ, and the finite and infinite formulations are equivalent:

• InfiniteGraph.relabel — relabeling by a permutation of ℕ (continuous, hence measurable);
• InfiniteGraph.exists_perm_extend — every injection Fin k ↪ ℕ extends to a permutation of ℕ (Equiv.Set.compl on the cofinite complements);
• Graphon.ExchangeableGraphLaw.infiniteLaw_map_relabel — exchangeability of the infinite law: every finite image lies in an initial segment, where injection consistency identifies the relabeled marginals, and uniqueness of the extension concludes;
• Graphon.InfiniteExchangeableGraphLaw — the measure-side object: a probability law on the infinite graph space invariant under every relabeling;
• Graphon.exchangeableGraphLawEquivInfinite — the headline equivalence ExchangeableGraphLaw ≃ InfiniteExchangeableGraphLaw, with finite marginals and the infinite extension as inverse maps.

This completes layers 1–2 of the Aldous–Hoover roadmap.

def InfiniteGraph.relabel (σ : Equiv.Perm ℕ) (G : InfiniteGraph) : InfiniteGraph

Relabeling of infinite graphs by a permutation of ℕ.

Equations

• InfiniteGraph.relabel σ G = SimpleGraph.comap (⇑σ) G

@[simp]

theorem InfiniteGraph.relabel_adj (σ : Equiv.Perm ℕ) (G : InfiniteGraph) (a b : ℕ) : (relabel σ G).Adj a b ↔ G.Adj (σ a) (σ b)

theorem InfiniteGraph.mem_edgeSet_relabel (σ : Equiv.Perm ℕ) (G : InfiniteGraph) (s : Sym2 ℕ) : s ∈ SimpleGraph.edgeSet (relabel σ G) ↔ Sym2.map (⇑σ) s ∈ SimpleGraph.edgeSet G

Edge membership under relabeling, in Sym2 form.

def InfiniteGraph.edgeIndexMap (σ : Equiv.Perm ℕ) (e : EdgeIndex) : EdgeIndex

The edge-index action of a permutation.

Equations

• InfiniteGraph.edgeIndexMap σ e = ⟨Sym2.map ⇑σ ↑e, ⋯⟩

theorem InfiniteGraph.continuous_relabel (σ : Equiv.Perm ℕ) : Continuous (relabel σ)

Relabeling is continuous: each output coordinate is an input coordinate.

theorem InfiniteGraph.measurable_relabel (σ : Equiv.Perm ℕ) : Measurable (relabel σ)

theorem InfiniteGraph.restrictFin_relabel {k n : ℕ} (σ : Equiv.Perm ℕ) (e : Fin k ↪ Fin n) (he : ∀ (a : Fin k), σ ↑a = ↑(e a)) (G : InfiniteGraph) : restrictFin k (relabel σ G) = SimpleGraph.comap (⇑e) (restrictFin n G)

Restricting a relabeled graph is comap along any finite embedding realizing the permutation on the initial segment.

theorem InfiniteGraph.exists_perm_extend {k : ℕ} (g : Fin k ↪ ℕ) : ∃ (σ : Equiv.Perm ℕ), ∀ (a : Fin k), σ ↑a = g a

Every injection of an initial segment into ℕ extends to a permutation — the shared graph-independent _root_.exists_perm_extend (Graphon.PermutationExtension).

theorem Graphon.ExchangeableGraphLaw.infiniteLaw_map_relabel (L : ExchangeableGraphLaw) (σ : Equiv.Perm ℕ) : MeasureTheory.Measure.map (InfiniteGraph.relabel σ) ↑L.infiniteLaw = ↑L.infiniteLaw

Exchangeability of the infinite law: the infinite law is invariant under every relabeling of ℕ. Every finite restriction of the relabeled law lands in an initial segment, where injection consistency identifies it with the marginal; uniqueness of the extension concludes.

structure Graphon.InfiniteExchangeableGraphLaw : Type

Infinite exchangeable graph laws: probability laws on the infinite graph space invariant under every relabeling of ℕ.

• law : MeasureTheory.ProbabilityMeasure InfiniteGraph

  The law on the infinite graph space.

• exchangeable (σ : Equiv.Perm ℕ) : MeasureTheory.Measure.map (InfiniteGraph.relabel σ) ↑self.law = ↑self.law

  Invariance under every relabeling.

theorem Graphon.InfiniteExchangeableGraphLaw.ext {M N : InfiniteExchangeableGraphLaw} (h : M.law = N.law) : M = N

theorem Graphon.InfiniteExchangeableGraphLaw.ext_iff {M N : InfiniteExchangeableGraphLaw} : M = N ↔ M.law = N.law

noncomputable def Graphon.InfiniteExchangeableGraphLaw.toExchangeableGraphLaw (M : InfiniteExchangeableGraphLaw) : ExchangeableGraphLaw

The finite marginals of an infinite exchangeable law form an exchangeable graph law: consistency under an arbitrary injection follows by extending it to a permutation of ℕ (exists_perm_extend) and applying exchangeability.

Equations

• M.toExchangeableGraphLaw = { law := fun (k : ℕ) => (MeasureTheory.Measure.map (InfiniteGraph.restrictFin k) ↑M.law).toPMF, consistent := ⋯ }

theorem Graphon.InfiniteExchangeableGraphLaw.toExchangeableGraphLaw_law (M : InfiniteExchangeableGraphLaw) (k : ℕ) : (M.toExchangeableGraphLaw.law k).toMeasure = MeasureTheory.Measure.map (InfiniteGraph.restrictFin k) ↑M.law

The finite marginals of the infinite law, unfolded.

noncomputable def Graphon.exchangeableGraphLawEquivInfinite : ExchangeableGraphLaw ≃ InfiniteExchangeableGraphLaw

The headline equivalence (Aldous–Hoover layers 1–2): exchangeable graph laws and infinite exchangeable graph laws are the same data, with finite marginals and the infinite extension as inverse maps.

Equations

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

@[simp]

theorem Graphon.exchangeableGraphLawEquivInfinite_apply_law (L : ExchangeableGraphLaw) : (exchangeableGraphLawEquivInfinite L).law = L.infiniteLaw