The infinite relational extension via compactness (AHK umbrella #103, R2b)

The compactness-based extension of a RelExchangeableLaw to a probability law on the infinite structure space realizing its marginals (issue #105), the multi-sorted analogue of Graphon.ExchangeableGraphLaw.infiniteLaw. Assumptions: [Fintype S.Srt] [Countable S.Rel] — raw-product compactness is countability-free, but the subsequential weak compactness runs through the metrizable ProbabilityMeasure topology, which uses the countable-coordinate Polish structure.

Route (exactly as planned): pad each diagonal marginal to the infinite space, extract a weakly convergent subsequence (the space is compact), and identify every size-vector marginal of the limit using continuity of the restriction (continuous_restrictFin), eventual domination (exists_const_ge), and consistency.

• RelExchangeableLaw.paddedLaw and paddedLaw_map_restrictFin — the diagonal padded laws and their finite restrictions (the combinatorial restrict_comp_pad / restrictFin_pad_diag identities live in RelationalStructure.lean);
• RelExchangeableLaw.exists_map_restrictFin_eq and infiniteLaw — the infinite relational extension: a weak subsequential limit whose finite restrictions are the given marginals (infiniteLaw_map_restrictFin).

Exchangeability of infiniteLaw is mathematically forced but is packaged and proved only in R2c, together with uniqueness and the finite/infinite-law equivalence.

theorem RelSignature.exists_subseq_tendsto {S : RelSignature} [Countable S.Rel] (Ps : ℕ → MeasureTheory.ProbabilityMeasure (S.RelStructure S.Vinfinite)) : ∃ (P : MeasureTheory.ProbabilityMeasure (S.RelStructure S.Vinfinite)) (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (Ps ∘ φ) Filter.atTop (nhds P)

Prokhorov extraction: on the (compact metrizable) infinite structure space, every sequence of probability measures has a weakly convergent subsequence.

noncomputable def RelSignature.RelExchangeableLaw.paddedLaw {S : RelSignature} (L : S.RelExchangeableLaw) (N : ℕ) : MeasureTheory.ProbabilityMeasure (S.RelStructure S.Vinfinite)

The diagonal padded law at level N: the N-diagonal marginal pushed forward to the infinite structure space through the value-embedding padding.

Equations

• L.paddedLaw N = ⟨MeasureTheory.Measure.map (RelSignature.RelStructure.pad fun (x : S.Srt) => Fin.valEmbedding) ↑(L.marginal fun (x : S.Srt) => N), ⋯⟩

@[simp]

theorem RelSignature.RelExchangeableLaw.paddedLaw_coe {S : RelSignature} (L : S.RelExchangeableLaw) (N : ℕ) : ↑(L.paddedLaw N) = MeasureTheory.Measure.map (RelStructure.pad fun (x : S.Srt) => Fin.valEmbedding) ↑(L.marginal fun (x : S.Srt) => N)

theorem RelSignature.RelExchangeableLaw.paddedLaw_map_restrictFin {S : RelSignature} (L : S.RelExchangeableLaw) {n : S.Srt → ℕ} {N : ℕ} (h : ∀ (s : S.Srt), n s ≤ N) : MeasureTheory.Measure.map (RelStructure.restrictFin n) ↑(L.paddedLaw N) = ↑(L.marginal n)

The finite restriction of the diagonal padded level-N law is exactly the n-marginal, for every size vector n ≤ N (by the padding/restriction identity and consistency).

theorem RelSignature.RelExchangeableLaw.exists_map_restrictFin_eq {S : RelSignature} [Fintype S.Srt] [Countable S.Rel] (L : S.RelExchangeableLaw) : ∃ (P : MeasureTheory.ProbabilityMeasure (S.RelStructure S.Vinfinite)), ∀ (n : S.Srt → ℕ), MeasureTheory.Measure.map (RelStructure.restrictFin n) ↑P = ↑(L.marginal n)

Existence of the infinite law: a weak subsequential limit of the diagonal padded laws has every finite restriction equal to the corresponding size-vector marginal.

noncomputable def RelSignature.RelExchangeableLaw.infiniteLaw {S : RelSignature} [Fintype S.Srt] [Countable S.Rel] (L : S.RelExchangeableLaw) : MeasureTheory.ProbabilityMeasure (S.RelStructure S.Vinfinite)

The infinite relational extension realizing the marginals (compactness Kolmogorov extension): a probability law on the infinite structure space whose finite restrictions are the given marginals. (Exchangeability is forced but is packaged/proved in R2c.)

Equations

• L.infiniteLaw = ⋯.choose

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

Marginal identification: each finite restriction of the infinite law is the corresponding size-vector marginal.