Exchangeable relational laws

An exchangeable random structure of a one-sorted relational language L on an unbounded vertex set has two presentations.

• Consistent finite marginals (ExchangeableRelationalLaw L): a probability law on the relational configurations on Fin k for every k, consistent under restriction along every injection Fin k ↪ Fin l. The permutations of Fin k give invariance under relabelling, and the inclusions Fin k ↪ Fin (k + 1) give projectivity.
• One invariant law on ℕ (InfiniteExchangeableRelationalLaw L): a probability law on the relational configurations on ℕ, invariant under restriction along every permutation of ℕ.

The two presentations agree (exchangeableRelationalLawEquivInfinite) when L has countably many relation symbols of each arity. From an infinite law, the marginals are its windows: the restrictions along Fin.val : Fin k → ℕ. Conversely, consistent marginals are the windows of a law over ℕ by Kolmogorov's extension theorem for configurations (TauCeti.RelationalConfiguration.exists_map_restrict_val_eq), which is unique because a finite measure on configurations over ℕ is determined by its windows (measure_ext_of_map_restrict_val).

The finitely supported permutations of ℕ act on configurations over ℕ by relabelling (TauCeti.RelationalConfiguration.instMulActionFinitaryPerm, in TauCeti.ModelTheory.RelationalConfiguration.Basic), and every exchangeable law on configurations over ℕ is invariant under this action. Ergodicity of the action on such a law, Mathlib's ErgodicSMul, is the relational counterpart of the ergodicity of exchangeable arrays.

Main definitions

• TauCeti.Probability.ExchangeableRelationalLaw — a consistent family of finite relational laws;
• TauCeti.Probability.InfiniteExchangeableRelationalLaw — a relabelling-invariant probability law on the configurations over ℕ;
• TauCeti.Probability.ExchangeableRelationalLaw.IsDissociated — restrictions to disjoint vertex windows are independent;
• TauCeti.Probability.exchangeableRelationalLawEquivInfinite — the two presentations agree.

Main results

• TauCeti.Probability.InfiniteExchangeableRelationalLaw.instSMulInvariantMeasureLaw — an exchangeable law on configurations over ℕ is invariant under finitary relabelling;
• TauCeti.Probability.exchangeableRelationalLawEquivInfinite_law_map_restrict — the windows of the infinite law attached to consistent marginals are those marginals;
• TauCeti.Probability.ExchangeableRelationalLaw.isDissociated_iff_forall_map_restrict_prod — a law is dissociated exactly when the restrictions of a marginal along any two injections with disjoint ranges are independent.

References

• O. Kallenberg, Probabilistic Symmetries and Invariance Principles, Springer, 2005, Chapter 7.
• P. Diaconis, S. Janson, Graph limits and exchangeable random graphs, Rend. Mat. Appl. (7) 28 (2008), 33--61, Section 5, for the case of graphs.
• The proof route adapts the graph case TauCeti.Combinatorics.DenseGraphLimits.ExchangeableGraphLaw.Infinite.Basic (exchangeableGraphLawEquivInfinite), which follows C. Freer, cameronfreer/graphon at commit 6eccca5bbe5c9df46d7129bf59575b8b9b1d6699, Apache-2.0, Graphon/InfiniteLaw.lean and Graphon/InfiniteExchangeability.lean. Here the Boolean edge coordinates of a graph are replaced by the Boolean atom coordinates of a configuration, and the extension of a window by false along Fin.val replaces the embedding of a finite graph into ℕ.

Consistent finite marginals

structure TauCeti.Probability.ExchangeableRelationalLaw (L : FirstOrder.Language) : Type u_2

An exchangeable random structure of L, presented by its consistent finite marginals: a probability law on the configurations on Fin k for every k, consistent under restriction along every injection of vertices.

• law (k : ℕ) : MeasureTheory.Measure (RelationalConfiguration L (Fin k))

  The level-k marginal law.

• prob (k : ℕ) : MeasureTheory.IsProbabilityMeasure (self.law k)

  Every marginal is a probability measure.

• consistent {k l : ℕ} (f : Fin k ↪ Fin l) : MeasureTheory.Measure.map (RelationalConfiguration.restrict ⇑f) (self.law l) = self.law k

  Consistency under restriction along every injection of vertices.

instance TauCeti.Probability.ExchangeableRelationalLaw.instIsProbabilityMeasureLaw {L : FirstOrder.Language} (μ : ExchangeableRelationalLaw L) (k : ℕ) : MeasureTheory.IsProbabilityMeasure (μ.law k)

theorem TauCeti.Probability.ExchangeableRelationalLaw.ext {L : FirstOrder.Language} {μ ν : ExchangeableRelationalLaw L} (h : ∀ (k : ℕ), μ.law k = ν.law k) : μ = ν

A law is determined by its marginals: the remaining fields are propositions.

theorem TauCeti.Probability.ExchangeableRelationalLaw.ext_iff {L : FirstOrder.Language} {μ ν : ExchangeableRelationalLaw L} : μ = ν ↔ ∀ (k : ℕ), μ.law k = ν.law k

Dissociation

def TauCeti.Probability.ExchangeableRelationalLaw.IsDissociated {L : FirstOrder.Language} (μ : ExchangeableRelationalLaw L) : Prop

An exchangeable relational law is dissociated when restrictions to disjoint vertex windows are independent: the level-(k + l) marginal, pushed to the pair of configurations it induces on the first k and on the last l vertices, is the product of the level-k and level-l marginals.

theorem TauCeti.Probability.ExchangeableRelationalLaw.isDissociated_iff {L : FirstOrder.Language} (μ : ExchangeableRelationalLaw L) : μ.IsDissociated ↔ ∀ (k l : ℕ), MeasureTheory.Measure.map (fun (c : RelationalConfiguration L (Fin (k + l))) => (RelationalConfiguration.restrict (Fin.castAdd l) c, RelationalConfiguration.restrict (Fin.natAdd k) c)) (μ.law (k + l)) = (μ.law k).prod (μ.law l)

The defining identity of a dissociated law.

theorem TauCeti.Probability.ExchangeableRelationalLaw.IsDissociated.map_restrict_prod {L : FirstOrder.Language} {μ : ExchangeableRelationalLaw L} (hμ : μ.IsDissociated) {k l n : ℕ} {f : Fin k → Fin n} {g : Fin l → Fin n} (hf : Function.Injective f) (hg : Function.Injective g) (hfg : ∀ (i : Fin k) (j : Fin l), f i ≠ g j) : MeasureTheory.Measure.map (fun (c : RelationalConfiguration L (Fin n)) => (RelationalConfiguration.restrict f c, RelationalConfiguration.restrict g c)) (μ.law n) = (μ.law k).prod (μ.law l)

Dissociated laws are independent on any two disjoint windows: the restrictions of the level-n marginal along two injections with disjoint ranges are independent, with the level-k and level-l marginals as laws.

theorem TauCeti.Probability.ExchangeableRelationalLaw.isDissociated_iff_forall_map_restrict_prod {L : FirstOrder.Language} (μ : ExchangeableRelationalLaw L) : μ.IsDissociated ↔ ∀ (k l n : ℕ) (f : Fin k → Fin n) (g : Fin l → Fin n), Function.Injective f → Function.Injective g → (∀ (i : Fin k) (j : Fin l), f i ≠ g j) → MeasureTheory.Measure.map (fun (c : RelationalConfiguration L (Fin n)) => (RelationalConfiguration.restrict f c, RelationalConfiguration.restrict g c)) (μ.law n) = (μ.law k).prod (μ.law l)

Dissociation on arbitrary disjoint windows. A law is dissociated exactly when the restrictions of every marginal along any two injections with disjoint ranges are independent, with the smaller marginals as laws.

Extension of the marginals to ℕ

Invariant laws on ℕ

structure TauCeti.Probability.InfiniteExchangeableRelationalLaw (L : FirstOrder.Language) : Type u_2

An exchangeable law on configurations over ℕ: a probability law on the relational configurations over ℕ invariant under relabelling along every permutation of ℕ.

• law : MeasureTheory.Measure (RelationalConfiguration L ℕ)

  The law on configurations over ℕ.

• prob : MeasureTheory.IsProbabilityMeasure self.law

  It is a probability measure.

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

  Invariance under every relabelling.

instance TauCeti.Probability.InfiniteExchangeableRelationalLaw.instIsProbabilityMeasureLaw {L : FirstOrder.Language} (μ : InfiniteExchangeableRelationalLaw L) : MeasureTheory.IsProbabilityMeasure μ.law

instance TauCeti.Probability.InfiniteExchangeableRelationalLaw.instSMulInvariantMeasureLaw {L : FirstOrder.Language} (μ : InfiniteExchangeableRelationalLaw L) : MeasureTheory.SMulInvariantMeasure FinitaryPerm (RelationalConfiguration L ℕ) μ.law

An exchangeable law on configurations over ℕ is invariant under finitary relabelling.

theorem TauCeti.Probability.InfiniteExchangeableRelationalLaw.ext {L : FirstOrder.Language} {μ ν : InfiniteExchangeableRelationalLaw L} (h : μ.law = ν.law) : μ = ν

An exchangeable law on configurations over ℕ is determined by its law: the other fields are propositions.

theorem TauCeti.Probability.InfiniteExchangeableRelationalLaw.ext_iff {L : FirstOrder.Language} {μ ν : InfiniteExchangeableRelationalLaw L} : μ = ν ↔ μ.law = ν.law

theorem TauCeti.Probability.InfiniteExchangeableRelationalLaw.map_restrict_val_map_restrict {L : FirstOrder.Language} (μ : InfiniteExchangeableRelationalLaw L) {k l : ℕ} (f : Fin k ↪ Fin l) : MeasureTheory.Measure.map (RelationalConfiguration.restrict ⇑f) (MeasureTheory.Measure.map (RelationalConfiguration.restrict Fin.val) μ.law) = MeasureTheory.Measure.map (RelationalConfiguration.restrict Fin.val) μ.law

The windows of an exchangeable law are consistent: restricting along an injection Fin k ↪ Fin l is relabelling along a permutation of ℕ extending it, followed by taking the smaller window.

The two presentations agree

noncomputable def TauCeti.Probability.exchangeableRelationalLawEquivInfinite (L : FirstOrder.Language) [∀ (n : ℕ), Countable (L.Relations n)] : ExchangeableRelationalLaw L ≃ InfiniteExchangeableRelationalLaw L

Consistent finite marginals are an exchangeable law on configurations over ℕ. For a language with countably many relation symbols of each arity, consistent marginals extend to a unique relabelling-invariant law over ℕ whose windows are those marginals; conversely the windows of such a law are consistent marginals.

@[simp]

theorem TauCeti.Probability.exchangeableRelationalLawEquivInfinite_law_map_restrict {L : FirstOrder.Language} [∀ (n : ℕ), Countable (L.Relations n)] (μ : ExchangeableRelationalLaw L) (k : ℕ) : MeasureTheory.Measure.map (RelationalConfiguration.restrict Fin.val) ((exchangeableRelationalLawEquivInfinite L) μ).law = μ.law k

The windows of the extension are the marginals.

@[simp]

theorem TauCeti.Probability.exchangeableRelationalLawEquivInfinite_symm_law {L : FirstOrder.Language} [∀ (n : ℕ), Countable (L.Relations n)] (μ : InfiniteExchangeableRelationalLaw L) (k : ℕ) : ((exchangeableRelationalLawEquivInfinite L).symm μ).law k = MeasureTheory.Measure.map (RelationalConfiguration.restrict Fin.val) μ.law

The marginals attached to an exchangeable law on configurations over ℕ are its windows.