The infinite relational-structure space (AHK umbrella #103, R1b)

The topological / measurable layer of the generic AHK carrier (issue #104). Because RelStructure S V = RelCoord S V → Bool is the Boolean product over the coordinate type, it inherits the product topology and the product σ-algebra directly. The product is compact with no countability assumption; under [Countable S.Rel] (and countable value carriers) the coordinate type is countable, so the space is additionally Polish and standard Borel. Over the product σ-algebra — again with no countability needed — its measurable structure is generated by the coordinate evaluations, hence by the finite-restriction cylinders; under those countability assumptions the product σ-algebra agrees with the Borel σ-algebra of the topology.

• RelSignature.instPolishSpace — the space is Polish under countability; compactness is inherited from the product with no countability assumption;
• RelSignature.measurable_restrictFin / measurable_restrictLE — the finite restrictions are measurable;
• RelSignature.cylinders — the finite-restriction cylinders, a π-system (isPiSystem_cylinders) generating the product σ-algebra (generateFrom_cylinders_eq);
• RelSignature.RelStructure.ext_of_map_restrictFin — finite-restriction measure extensionality: two finite measures on the infinite structure space agree once all their finite-restriction pushforwards agree.
• RelSignature.continuous_comap and its corollaries continuous_restrict / continuous_relabel / continuous_restrictFin / continuous_restrictLE, plus continuous_pad / measurable_pad — continuity (and measurability) of the sortwise actions, needed for the R2 compactness-extension route.

No projective extension here — that is R2.

Polish / standard-Borel structure

instance RelSignature.instPolishSpace {S : RelSignature} [Countable S.Rel] {V : S.Srt → Type u_1} [∀ (s : S.Srt), Countable (V s)] : PolishSpace (S.RelStructure V)

The infinite structure space is Polish (a countable Boolean product). Compact, metrizable, second-countable, Borel, and standard-Borel are inherited from the product.

Measurability of the restrictions (over the product σ-algebra)

theorem RelSignature.measurable_eval {S : RelSignature} {V : S.Srt → Type u_1} (c : S.RelCoord V) : Measurable fun (σ : S.RelStructure V) => σ c

Coordinate evaluation is measurable.

theorem RelSignature.measurable_restrictFin {S : RelSignature} (n : S.Srt → ℕ) : Measurable (RelStructure.restrictFin n)

Finite restriction is measurable: each of its coordinates is a coordinate evaluation of the original structure.

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

Restriction between size vectors is measurable.

theorem RelSignature.measurable_restrict {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (e : (s : S.Srt) → V s ↪ W s) : Measurable (RelStructure.restrict e)

Restriction along a sortwise family of embeddings is measurable (over the product σ-algebra; no countability needed).

theorem RelSignature.measurable_relabel {S : RelSignature} {V : S.Srt → Type u_1} (σ : (s : S.Srt) → Equiv.Perm (V s)) : Measurable (RelStructure.relabel σ)

Relabelling by a sortwise family of permutations is measurable.

The finite-restriction cylinders

def RelSignature.cylinders (S : RelSignature) : Set (Set (S.RelStructure S.Vinfinite))

The finite-restriction cylinders: preimages of measurable finite-level events.

Equations

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

theorem RelSignature.restrictFin_preimage_restrictLE {S : RelSignature} {n m : S.Srt → ℕ} (h : ∀ (s : S.Srt), n s ≤ m s) (T : Set (S.RelStructure (Vfinite n))) : RelStructure.restrictFin n ⁻¹' T = RelStructure.restrictFin m ⁻¹' RelStructure.restrictLE h ⁻¹' T

A lower-level cylinder is a higher-level cylinder.

theorem RelSignature.isPiSystem_cylinders {S : RelSignature} : IsPiSystem S.cylinders

The cylinders form a π-system (align two size vectors at their pointwise maximum).

theorem RelSignature.exists_restrictFin_eval {S : RelSignature} (c : S.RelCoord S.Vinfinite) : ∃ (n : S.Srt → ℕ) (c' : S.RelCoord (Vfinite n)), ∀ (σ : S.RelStructure S.Vinfinite), σ c = RelStructure.restrictFin n σ c'

Every coordinate evaluation factors through a finite restriction.

theorem RelSignature.generateFrom_cylinders_eq {S : RelSignature} : MeasurableSpace.generateFrom S.cylinders = inferInstance

The cylinders generate the product measurable space of the infinite structure space — the coordinate evaluations each factor through a finite restriction. (Under the countability assumptions yielding the Polish instance, this product σ-algebra agrees with the Borel σ-algebra of the product topology; the statement itself needs no countability.)

theorem RelSignature.RelStructure.ext_of_map_restrictFin {S : RelSignature} {μ ν : MeasureTheory.Measure (S.RelStructure S.Vinfinite)} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (n : S.Srt → ℕ), MeasureTheory.Measure.map (restrictFin n) μ = MeasureTheory.Measure.map (restrictFin n) ν) : μ = ν

Finite-restriction measure extensionality: two finite measures on the infinite structure space with equal pushforwards under every finite restriction are equal.

Continuity of the sortwise actions

Needed by R2's compactness-extension route: identifying the finite marginals of a weak limit uses continuity of the restriction maps, not just measurability.

theorem RelSignature.continuous_comap {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (f : (s : S.Srt) → V s → W s) : Continuous (RelStructure.comap f)

The sortwise pullback is continuous: comap f σ = σ ∘ RelCoord.map f is a precomposition, hence continuous coordinatewise. This is the reusable primitive.

theorem RelSignature.continuous_restrict {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (e : (s : S.Srt) → V s ↪ W s) : Continuous (RelStructure.restrict e)

Restriction to a sub-carrier is continuous.

theorem RelSignature.continuous_relabel {S : RelSignature} {V : S.Srt → Type u_1} (σ : (s : S.Srt) → Equiv.Perm (V s)) : Continuous (RelStructure.relabel σ)

Relabelling is continuous.

theorem RelSignature.continuous_restrictFin {S : RelSignature} (n : S.Srt → ℕ) : Continuous (RelStructure.restrictFin n)

Finite restriction is continuous.

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

Restriction between size vectors is continuous.

theorem RelSignature.continuous_pad {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (e : (s : S.Srt) → V s ↪ W s) : Continuous (RelStructure.pad e)

Padding is continuous: for each coordinate the padded value is, on a fixed membership condition, either a coordinate evaluation or the constant false.

theorem RelSignature.measurable_pad {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (e : (s : S.Srt) → V s ↪ W s) : Measurable (RelStructure.pad e)

Padding is measurable (over the product σ-algebra; no countability needed) — the measurable counterpart of continuous_pad.