Exchangeable graph laws as exchangeable relational laws

Encoding a simple graph as a configuration of the language of graphs (SimpleGraph.toRelationalConfiguration) turns an exchangeable graph law into an exchangeable relational law, and an exchangeable law on infinite graphs into an invariant relational law on ℕ. The generic correspondence between the two presentations of exchangeable relational laws (TauCeti.Probability.exchangeableRelationalLawEquivInfinite) then agrees with the graph-specific one (exchangeableGraphLawEquivInfinite): extending the encoded finite marginals gives the encoding of the extended graph law.

Conversely, the encoding identifies exchangeable graph laws with the exchangeable relational laws of the language of graphs whose marginals are concentrated on simple graphs, and likewise for laws on infinite graphs: laws on simple graphs are recovered from their encodings by pulling back along the encoding, a measurable embedding on countable vertex types.

Main definitions

• TauCeti.DenseGraphLimits.ExchangeableGraphLaw.toRelationalLaw — the exchangeable relational law of an exchangeable graph law;
• TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.toRelationalLaw — the invariant relational law on ℕ of an exchangeable law on infinite graphs;
• TauCeti.DenseGraphLimits.ExchangeableGraphLaw.relationalLawEquiv and TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.relationalLawEquiv — these encodings are equivalences onto the relational laws concentrated on simple graphs.

Main results

• ExchangeableGraphLaw.exchangeableRelationalLawEquivInfinite_toRelationalLaw (in TauCeti.DenseGraphLimits) — the generic correspondence agrees with exchangeableGraphLawEquivInfinite;
• ae_isSimpleGraph_exchangeableRelationalLawEquivInfinite_law_iff (in TauCeti.DenseGraphLimits) — the generic correspondence matches relational laws concentrated on simple graphs on both sides.

noncomputable def TauCeti.DenseGraphLimits.ExchangeableGraphLaw.toRelationalLaw (L : ExchangeableGraphLaw) : Probability.ExchangeableRelationalLaw FirstOrder.Language.graph

The exchangeable relational law of an exchangeable graph law: its marginals, encoded as configurations of the language of graphs.

@[simp]

theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.toRelationalLaw_law (L : ExchangeableGraphLaw) (n : ℕ) : L.toRelationalLaw.law n = MeasureTheory.Measure.map SimpleGraph.toRelationalConfiguration (L.law n)

theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.ae_isSimpleGraph_toRelationalLaw_law (L : ExchangeableGraphLaw) (n : ℕ) : ∀ᵐ (c : RelationalConfiguration FirstOrder.Language.graph (Fin n)) ∂L.toRelationalLaw.law n, c.IsSimpleGraph

The marginals of the relational law of an exchangeable graph law are concentrated on simple graphs.

noncomputable def TauCeti.DenseGraphLimits.ExchangeableGraphLaw.relationalLawEquiv : ExchangeableGraphLaw ≃ { μ : Probability.ExchangeableRelationalLaw FirstOrder.Language.graph // ∀ (n : ℕ), ∀ᵐ (c : RelationalConfiguration FirstOrder.Language.graph (Fin n)) ∂μ.law n, c.IsSimpleGraph }

Exchangeable graph laws are the exchangeable relational laws of the language of graphs whose marginals are concentrated on simple graphs, that is, on symmetric irreflexive configurations. The inverse pulls each marginal back along the encoding.

@[simp]

theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.coe_relationalLawEquiv (L : ExchangeableGraphLaw) : ↑(relationalLawEquiv L) = L.toRelationalLaw

@[simp]

theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.relationalLawEquiv_symm_law (μ : { μ : Probability.ExchangeableRelationalLaw FirstOrder.Language.graph // ∀ (n : ℕ), ∀ᵐ (c : RelationalConfiguration FirstOrder.Language.graph (Fin n)) ∂μ.law n, c.IsSimpleGraph }) (n : ℕ) : (relationalLawEquiv.symm μ).law n = MeasureTheory.Measure.comap SimpleGraph.toRelationalConfiguration ((↑μ).law n)

theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.toRelationalLaw_injective : Function.Injective toRelationalLaw

Distinct exchangeable graph laws have distinct relational laws.

noncomputable def TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.toRelationalLaw (L : InfiniteExchangeableGraphLaw) : Probability.InfiniteExchangeableRelationalLaw FirstOrder.Language.graph

The invariant relational law of an exchangeable law on infinite graphs: its law, encoded as configurations of the language of graphs.

@[simp]

theorem TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.toRelationalLaw_law (L : InfiniteExchangeableGraphLaw) : L.toRelationalLaw.law = MeasureTheory.Measure.map SimpleGraph.toRelationalConfiguration L.law

theorem TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.ae_isSimpleGraph_toRelationalLaw_law (L : InfiniteExchangeableGraphLaw) : ∀ᵐ (c : RelationalConfiguration FirstOrder.Language.graph ℕ) ∂L.toRelationalLaw.law, c.IsSimpleGraph

The relational law of an exchangeable law on infinite graphs is concentrated on simple graphs.

noncomputable def TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.relationalLawEquiv : InfiniteExchangeableGraphLaw ≃ { μ : Probability.InfiniteExchangeableRelationalLaw FirstOrder.Language.graph // ∀ᵐ (c : RelationalConfiguration FirstOrder.Language.graph ℕ) ∂μ.law, c.IsSimpleGraph }

Exchangeable laws on infinite graphs are the exchangeable relational laws of the language of graphs on ℕ concentrated on simple graphs, that is, on symmetric irreflexive configurations. The inverse pulls the law back along the encoding.

@[simp]

theorem TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.coe_relationalLawEquiv (L : InfiniteExchangeableGraphLaw) : ↑(relationalLawEquiv L) = L.toRelationalLaw

@[simp]

theorem TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.relationalLawEquiv_symm_law (μ : { μ : Probability.InfiniteExchangeableRelationalLaw FirstOrder.Language.graph // ∀ᵐ (c : RelationalConfiguration FirstOrder.Language.graph ℕ) ∂μ.law, c.IsSimpleGraph }) : (relationalLawEquiv.symm μ).law = MeasureTheory.Measure.comap SimpleGraph.toRelationalConfiguration (↑μ).law

theorem TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.toRelationalLaw_injective : Function.Injective toRelationalLaw

Distinct exchangeable laws on infinite graphs have distinct relational laws.

theorem TauCeti.DenseGraphLimits.ExchangeableGraphLaw.exchangeableRelationalLawEquivInfinite_toRelationalLaw (L : ExchangeableGraphLaw) : (Probability.exchangeableRelationalLawEquivInfinite FirstOrder.Language.graph) L.toRelationalLaw = (exchangeableGraphLawEquivInfinite L).toRelationalLaw

The generic correspondence agrees with the graph-specific one: extending the relational law of an exchangeable graph law gives the relational law of its extension to infinite graphs.

theorem TauCeti.DenseGraphLimits.ae_isSimpleGraph_exchangeableRelationalLawEquivInfinite_law_iff (μ : Probability.ExchangeableRelationalLaw FirstOrder.Language.graph) : (∀ᵐ (c : RelationalConfiguration FirstOrder.Language.graph ℕ) ∂((Probability.exchangeableRelationalLawEquivInfinite FirstOrder.Language.graph) μ).law, c.IsSimpleGraph) ↔ ∀ (n : ℕ), ∀ᵐ (c : RelationalConfiguration FirstOrder.Language.graph (Fin n)) ∂μ.law n, c.IsSimpleGraph

Consistent marginals concentrated on simple graphs extend to a law concentrated on simple graphs, and conversely: the extension of an exchangeable relational law of the language of graphs is concentrated on simple graphs exactly when every marginal is.