Exchangeable relational laws: size-vector marginals and consistency (AHK umbrella #103, R2a)

The finite-marginal layer of the generic exchangeable-law theory (issue #105). A generic exchangeable law is given by a size-vector-indexed family of probability marginals that is consistent under arbitrary sortwise injections — the multi-sorted, arbitrary-arity analogue of Graphon.ExchangeableGraphLaw.

Crucially the finite marginals are ProbabilityMeasure (RelStructure S (Vfinite n)), not PMF: with countably many relation symbols a finite vertex carrier still has infinitely many Boolean coordinates, so RelStructure S (Vfinite n) can be an (uncountable) standard-Borel space and the law can be non-atomic. (D2 recovers PMFs in the finite-signature case.)

• RelSignature.exists_const_ge — because S.Srt is finite, the diagonal size vectors are cofinal (every size vector is bounded by a constant one);
• RelSignature.RelExchangeableLaw — the structure: probability marginals + arbitrary sortwise-injection consistency;
• RelExchangeableLaw.marginal_map_restrictLE / marginal_map_perm — consistency under the standard size-vector inclusion, and finite exchangeability (permutation invariance) of the marginals, both special cases.

The compactness-based extension to an infinite law is R2b; uniqueness (via ext_of_map_restrictFin) and the finite/infinite equivalence are R2c.

theorem RelSignature.exists_const_ge {S : RelSignature} [Fintype S.Srt] (n : S.Srt → ℕ) : ∃ (N : ℕ), ∀ (s : S.Srt), n s ≤ N

Diagonal cofinality: since S.Srt is finite, every size vector is bounded above by a constant (diagonal) size vector — so diagonal marginals suffice for the extension.

structure RelSignature.RelExchangeableLaw (S : RelSignature) : Type u_1

An exchangeable relational law: a size-vector-indexed family of probability marginals on the finite structure spaces, consistent under every sortwise injection ∀ s, Fin (n s) ↪ Fin (m s) (the m-marginal restricts to the n-marginal).

• marginal (n : S.Srt → ℕ) : MeasureTheory.ProbabilityMeasure (S.RelStructure (Vfinite n))

  The probability marginal on structures over the size vector n.

• consistent {n m : S.Srt → ℕ} (e : (s : S.Srt) → Fin (n s) ↪ Fin (m s)) : MeasureTheory.Measure.map (RelStructure.restrict e) ↑(self.marginal m) = ↑(self.marginal n)

  Consistency under every sortwise injection.

theorem RelSignature.RelExchangeableLaw.ext {S : RelSignature} {x y : S.RelExchangeableLaw} (marginal : x.marginal = y.marginal) : x = y

theorem RelSignature.RelExchangeableLaw.ext_iff {S : RelSignature} {x y : S.RelExchangeableLaw} : x = y ↔ x.marginal = y.marginal

theorem RelSignature.RelExchangeableLaw.marginal_map_restrictLE {S : RelSignature} (L : S.RelExchangeableLaw) {n m : S.Srt → ℕ} (h : ∀ (s : S.Srt), n s ≤ m s) : MeasureTheory.Measure.map (RelStructure.restrictLE h) ↑(L.marginal m) = ↑(L.marginal n)

Consistency under the standard size-vector inclusion n ≤ m.

theorem RelSignature.RelExchangeableLaw.marginal_map_perm {S : RelSignature} (L : S.RelExchangeableLaw) {n : S.Srt → ℕ} (σ : (s : S.Srt) → Equiv.Perm (Fin (n s))) : MeasureTheory.Measure.map (RelStructure.relabel σ) ↑(L.marginal n) = ↑(L.marginal n)

Finite exchangeability: each marginal is invariant under the sortwise permutations of its finite vertex sets — the special case n = m, e a permutation.