The finite/infinite exchangeable relational law equivalence (AHK umbrella #103, R2c)

The exchangeability, uniqueness, and finite/infinite-law equivalence completing R2 (issue #105), the multi-sorted analogue of Graphon.InfiniteExchangeability. Assumptions [Fintype S.Srt] [Countable S.Rel].

• RelExchangeableLaw.infiniteLaw_map_restrict — the arbitrary sortwise injection marginal theorem: map (restrict e) infiniteLaw = marginal n for any e : ∀ s, Fin (n s) ↪ ℕ (each finite range factors through a large size vector);
• RelSignature.InfiniteRelExchangeableLaw — a probability law on the infinite structure space invariant under every sortwise Equiv.Perm ℕ;
• RelExchangeableLaw.infiniteLaw_map_relabel / toInfinite — the infinite law is exchangeable, giving the forward map;
• InfiniteRelExchangeableLaw.toFinite — the reverse map (finite marginals of an exchangeable infinite law, consistent by the permutation extension exists_perm_extend, now shared from Graphon.PermutationExtension);
• RelSignature.relExchangeableLawEquiv — the equivalence RelExchangeableLaw S ≃ InfiniteRelExchangeableLaw S.

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

A probability law on the infinite structure space invariant under every sortwise permutation of ℕ.

• law : MeasureTheory.ProbabilityMeasure (S.RelStructure S.Vinfinite)

  The law on the infinite structure space.

• exchangeable (σ : S.Srt → Equiv.Perm ℕ) : MeasureTheory.Measure.map (RelStructure.relabel σ) ↑self.law = ↑self.law

  Invariance under every sortwise relabelling.

theorem RelSignature.InfiniteRelExchangeableLaw.ext_iff {S : RelSignature} {x y : S.InfiniteRelExchangeableLaw} : x = y ↔ x.law = y.law

theorem RelSignature.InfiniteRelExchangeableLaw.ext {S : RelSignature} {x y : S.InfiniteRelExchangeableLaw} (law : x.law = y.law) : x = y

theorem RelSignature.RelExchangeableLaw.infiniteLaw_map_restrict {S : RelSignature} [Fintype S.Srt] [Countable S.Rel] (L : S.RelExchangeableLaw) {n : S.Srt → ℕ} (e : (s : S.Srt) → Fin (n s) ↪ ℕ) : MeasureTheory.Measure.map (RelStructure.restrict e) ↑L.infiniteLaw = ↑(L.marginal n)

The arbitrary-injection marginal theorem: for any sortwise injection into ℕ, the pushforward of the infinite law is the finite marginal (each finite range factors through a large enough diagonal size vector).

theorem RelSignature.RelExchangeableLaw.infiniteLaw_map_relabel {S : RelSignature} [Fintype S.Srt] [Countable S.Rel] (L : S.RelExchangeableLaw) (σ : S.Srt → Equiv.Perm ℕ) : MeasureTheory.Measure.map (RelStructure.relabel σ) ↑L.infiniteLaw = ↑L.infiniteLaw

Exchangeability of the infinite law: it is invariant under every sortwise permutation of ℕ. Each finite restriction of the relabelled law is a restriction along an injection into ℕ, identified with the marginal by infiniteLaw_map_restrict; uniqueness concludes.

noncomputable def RelSignature.RelExchangeableLaw.toInfinite {S : RelSignature} [Fintype S.Srt] [Countable S.Rel] (L : S.RelExchangeableLaw) : S.InfiniteRelExchangeableLaw

The forward map: the infinite exchangeable relational law of an exchangeable law.

Equations

• L.toInfinite = { law := L.infiniteLaw, exchangeable := ⋯ }

@[simp]

theorem RelSignature.RelExchangeableLaw.toInfinite_law_map_restrictFin {S : RelSignature} [Fintype S.Srt] [Countable S.Rel] (L : S.RelExchangeableLaw) (n : S.Srt → ℕ) : MeasureTheory.Measure.map (RelStructure.restrictFin n) ↑L.toInfinite.law = ↑(L.marginal n)

noncomputable def RelSignature.InfiniteRelExchangeableLaw.marginal {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) (n : S.Srt → ℕ) : MeasureTheory.ProbabilityMeasure (S.RelStructure (Vfinite n))

The finite n-marginal of an infinite exchangeable law.

Equations

• M.marginal n = ⟨MeasureTheory.Measure.map (RelSignature.RelStructure.restrictFin n) ↑M.law, ⋯⟩

@[simp]

theorem RelSignature.InfiniteRelExchangeableLaw.marginal_coe {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) (n : S.Srt → ℕ) : ↑(M.marginal n) = MeasureTheory.Measure.map (RelStructure.restrictFin n) ↑M.law

noncomputable def RelSignature.InfiniteRelExchangeableLaw.toFinite {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) : S.RelExchangeableLaw

The reverse map: the finite marginals of an exchangeable infinite law form an exchangeable law. Consistency under a sortwise injection follows from exchangeability: the injection extends (per sort) to a permutation of ℕ, and invariance under it identifies the restricted marginal.

Equations

• M.toFinite = { marginal := M.marginal, consistent := ⋯ }

noncomputable def RelSignature.relExchangeableLawEquiv {S : RelSignature} [Fintype S.Srt] [Countable S.Rel] : S.RelExchangeableLaw ≃ S.InfiniteRelExchangeableLaw

The finite/infinite exchangeable relational law equivalence (R2c): exchangeable size-vector marginal families correspond exactly to probability laws on the infinite structure space invariant under sortwise relabelling.

Equations

• RelSignature.relExchangeableLawEquiv = { toFun := RelSignature.RelExchangeableLaw.toInfinite, invFun := RelSignature.InfiniteRelExchangeableLaw.toFinite, left_inv := ⋯, right_inv := ⋯ }