Sortwise disjoint-block restrictions and finite-event factorization (AHK umbrella, R3a / #106)

The block machinery for the generic relational extremality theory: sortwise vertex shifts and disjoint-block restrictions of the infinite structure space, the initial / tail / vertex-tail σ-algebras, invariance of an exchangeable law under arbitrary injective relabelings and under the shift, and dissociation as exact finite-event (block) factorization:

• RelStructure.drop k — the sortwise vertex shift (forget the first k s vertices of each sort), with shiftEmb k l the embedding of the next l-block after k;
• InfiniteRelExchangeableLaw.law_map_restrict — the law of any sortwise injective restriction depends only on the block sizes (extend to a permutation, use exchangeability);
• InfiniteRelExchangeableLaw.law_map_drop — shift invariance of the law;
• RelStructure.initialAlgebra / tailAlgebra / vertexTailAlgebra — the σ-algebras of the first-block, after-block, and tail events (the vertex tail as the meet over all size vectors, equal to the diagonal meet under Fintype S.Srt), with monotonicity, iSup_initialAlgebra_eq (the initial algebras generate), and the finite tail windows tailWindowAlgebra exhausting tailAlgebra (iSup_tailWindowAlgebra_eq);
• InfiniteRelExchangeableLaw.IsDissociated — exact finite-event factorization: the joint law of the block pair (blockPair) is the product of the two marginals, for all block sizes; by IsDissociated.map_restrict_pair this factorizes arbitrary sortwise injections with disjoint ranges, not only the canonical adjacent blocks.

This generalizes the undirected Graphon/RestrictionIndependence.lean design to arbitrary finite-sort, countable-relation signatures. The equivalences (dissociated ↔ restriction- independent ↔ tail-trivial, and the extreme/ergodic items) are R3b/R3c.

The sortwise shift and block embeddings

def RelSignature.RelStructure.drop {S : RelSignature} (k : S.Srt → ℕ) : S.RelStructure S.Vinfinite → S.RelStructure S.Vinfinite

The sortwise vertex shift: forget the first k s vertices of each sort.

Equations

• RelSignature.RelStructure.drop k = RelSignature.RelStructure.comap fun (s : S.Srt) (n : ℕ) => n + k s

theorem RelSignature.measurable_drop {S : RelSignature} (k : S.Srt → ℕ) : Measurable (RelStructure.drop k)

def RelSignature.shiftEmb {S : RelSignature} (k l : S.Srt → ℕ) (s : S.Srt) : Fin (l s) ↪ ℕ

The l-block after k: the sortwise embedding of Fin (l s) onto the vertices k s, k s + 1, … of each sort.

Equations

• RelSignature.shiftEmb k l s = { toFun := fun (i : Fin (l s)) => ↑i + k s, inj' := ⋯ }

theorem RelSignature.restrict_shiftEmb_eq {S : RelSignature} (k l : S.Srt → ℕ) : RelStructure.restrict (shiftEmb k l) = RelStructure.restrictFin l ∘ RelStructure.drop k

Restricting to the l-block after k is restricting the shifted structure to its initial l-block.

Restriction and shift invariance of an exchangeable law

theorem RelSignature.InfiniteRelExchangeableLaw.law_map_restrict {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) {n : S.Srt → ℕ} (e : (s : S.Srt) → Fin (n s) ↪ ℕ) : MeasureTheory.Measure.map (RelStructure.restrict e) ↑M.law = MeasureTheory.Measure.map (RelStructure.restrictFin n) ↑M.law

The law of any sortwise injective restriction depends only on the block sizes: extend each injection to a permutation of ℕ and use exchangeability.

theorem RelSignature.InfiniteRelExchangeableLaw.law_map_restrict_self {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) (e : (s : S.Srt) → S.Vinfinite s ↪ S.Vinfinite s) : MeasureTheory.Measure.map (RelStructure.restrict e) ↑M.law = ↑M.law

The law of any sortwise injective self-restriction is the law: every finite restriction of both sides agrees, because restricting a self-restriction is restricting along the composed finite embedding, whose law depends only on the block sizes.

theorem RelSignature.InfiniteRelExchangeableLaw.law_map_drop {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) (k : S.Srt → ℕ) : MeasureTheory.Measure.map (RelStructure.drop k) ↑M.law = ↑M.law

Shift invariance: forgetting the first k-block does not change the law — the shift is a sortwise injective self-restriction.

The initial, after-block, and vertex-tail σ-algebras

@[reducible]

noncomputable def RelSignature.RelStructure.initialAlgebra {S : RelSignature} (n : S.Srt → ℕ) : MeasurableSpace (S.RelStructure S.Vinfinite)

The initial σ-algebra: events depending only on the first n-block.

Equations

• RelSignature.RelStructure.initialAlgebra n = MeasurableSpace.comap (RelSignature.RelStructure.restrictFin n) inferInstance

theorem RelSignature.RelStructure.initialAlgebra_le {S : RelSignature} (n : S.Srt → ℕ) : initialAlgebra n ≤ inferInstance

theorem RelSignature.RelStructure.initialAlgebra_mono {S : RelSignature} {n m : S.Srt → ℕ} (h : ∀ (s : S.Srt), n s ≤ m s) : initialAlgebra n ≤ initialAlgebra m

The initial σ-algebras are monotone in the block sizes.

theorem RelSignature.RelStructure.iSup_initialAlgebra_eq {S : RelSignature} : ⨆ (n : S.Srt → ℕ), initialAlgebra n = inferInstance

The initial σ-algebras generate: every cylinder is an initial event.

@[reducible]

noncomputable def RelSignature.RelStructure.tailAlgebra {S : RelSignature} (k : S.Srt → ℕ) : MeasurableSpace (S.RelStructure S.Vinfinite)

The after-block σ-algebra: events depending only on the vertices after the first k-block.

Equations

• RelSignature.RelStructure.tailAlgebra k = MeasurableSpace.comap (RelSignature.RelStructure.drop k) inferInstance

theorem RelSignature.RelStructure.tailAlgebra_le {S : RelSignature} (k : S.Srt → ℕ) : tailAlgebra k ≤ inferInstance

theorem RelSignature.RelStructure.tailAlgebra_antitone {S : RelSignature} {k m : S.Srt → ℕ} (h : ∀ (s : S.Srt), k s ≤ m s) : tailAlgebra m ≤ tailAlgebra k

The after-block σ-algebras are antitone (along the diagonal it suffices to shift more).

@[reducible]

noncomputable def RelSignature.RelStructure.vertexTailAlgebra {S : RelSignature} : MeasurableSpace (S.RelStructure S.Vinfinite)

The vertex-tail σ-algebra: events measurable after forgetting any initial block (the meet over all size vectors).

Equations

• RelSignature.RelStructure.vertexTailAlgebra = ⨅ (k : S.Srt → ℕ), RelSignature.RelStructure.tailAlgebra k

theorem RelSignature.RelStructure.vertexTailAlgebra_le_tailAlgebra {S : RelSignature} (k : S.Srt → ℕ) : vertexTailAlgebra ≤ tailAlgebra k

theorem RelSignature.RelStructure.vertexTailAlgebra_le {S : RelSignature} : vertexTailAlgebra ≤ inferInstance

theorem RelSignature.RelStructure.vertexTailAlgebra_eq_iInf_diagonal {S : RelSignature} [Fintype S.Srt] : vertexTailAlgebra = ⨅ (k : ℕ), tailAlgebra fun (x : S.Srt) => k

The diagonal blocks are cofinal (Fintype S.Srt): the vertex-tail σ-algebra is already the meet over the diagonal size vectors.

@[reducible]

noncomputable def RelSignature.RelStructure.tailWindowAlgebra {S : RelSignature} (k l : S.Srt → ℕ) : MeasurableSpace (S.RelStructure S.Vinfinite)

The finite tail window: events depending only on the l-block after k.

Equations

• RelSignature.RelStructure.tailWindowAlgebra k l = MeasurableSpace.comap (RelSignature.RelStructure.restrict (RelSignature.shiftEmb k l)) inferInstance

theorem RelSignature.RelStructure.iSup_tailWindowAlgebra_eq {S : RelSignature} (k : S.Srt → ℕ) : ⨆ (l : S.Srt → ℕ), tailWindowAlgebra k l = tailAlgebra k

The finite tail windows exhaust the after-block σ-algebra: pull the generation of the Borel σ-algebra by initial blocks back through the shift.

Dissociation: exact finite-event factorization

def RelSignature.blockPair {S : RelSignature} (k l : S.Srt → ℕ) (X : S.RelStructure S.Vinfinite) : S.RelStructure (Vfinite k) × S.RelStructure (Vfinite l)

The joint block map: the first k-block together with the following l-block.

Equations

• RelSignature.blockPair k l X = (RelSignature.RelStructure.restrictFin k X, RelSignature.RelStructure.restrict (RelSignature.shiftEmb k l) X)

def RelSignature.InfiniteRelExchangeableLaw.IsDissociated {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) : Prop

Dissociation (exact finite-event factorization): for all block sizes k, l, the joint law of the first k-block and the following l-block is the product of the k- and l-marginals of the law.

Equations

• One or more equations did not get rendered due to their size.

theorem RelSignature.measurable_blockPair {S : RelSignature} (k l : S.Srt → ℕ) : Measurable (blockPair k l)

The joint block map is measurable.

theorem RelSignature.InfiniteRelExchangeableLaw.map_blockPair_fst {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) (k l : S.Srt → ℕ) : MeasureTheory.Measure.map Prod.fst (MeasureTheory.Measure.map (blockPair k l) ↑M.law) = MeasureTheory.Measure.map (RelStructure.restrictFin k) ↑M.law

The marginals of the joint block law are the block-size marginals of the law — independently of any dissociation hypothesis (first coordinate directly; second by the labeling-free restriction invariance).

theorem RelSignature.InfiniteRelExchangeableLaw.map_blockPair_snd {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) (k l : S.Srt → ℕ) : MeasureTheory.Measure.map Prod.snd (MeasureTheory.Measure.map (blockPair k l) ↑M.law) = MeasureTheory.Measure.map (RelStructure.restrictFin l) ↑M.law

theorem RelSignature.InfiniteRelExchangeableLaw.law_map_restrict_pair {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) {n m : S.Srt → ℕ} (e : (s : S.Srt) → Fin (n s) ↪ ℕ) (f : (s : S.Srt) → Fin (m s) ↪ ℕ) (hd : ∀ (s : S.Srt) (i : Fin (n s)) (j : Fin (m s)), (e s) i ≠ (f s) j) : MeasureTheory.Measure.map (fun (X : S.RelStructure fun (s : S.Srt) => ℕ) => (RelStructure.restrict e X, RelStructure.restrict f X)) ↑M.law = MeasureTheory.Measure.map (blockPair n m) ↑M.law

The joint law of disjoint blocks depends only on the block sizes (pure exchangeability, no dissociation): any two sortwise injections with disjoint ranges are, up to a relabeling, the canonical adjacent blocks.

theorem RelSignature.InfiniteRelExchangeableLaw.IsDissociated.map_restrict_pair {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (hM : M.IsDissociated) {n m : S.Srt → ℕ} (e : (s : S.Srt) → Fin (n s) ↪ ℕ) (f : (s : S.Srt) → Fin (m s) ↪ ℕ) (hd : ∀ (s : S.Srt) (i : Fin (n s)) (j : Fin (m s)), (e s) i ≠ (f s) j) : MeasureTheory.Measure.map (fun (X : S.RelStructure fun (s : S.Srt) => ℕ) => (RelStructure.restrict e X, RelStructure.restrict f X)) ↑M.law = (MeasureTheory.Measure.map (RelStructure.restrictFin n) ↑M.law).prod (MeasureTheory.Measure.map (RelStructure.restrictFin m) ↑M.law)

Dissociation factorizes arbitrary disjoint blocks: for any two sortwise injections with disjoint ranges, the joint law of the two restrictions is the product of the block-size marginals.