The infinite graph space (Aldous–Hoover layer 1, brick A1)

Simple graphs on ℕ as a compact metrizable zero-dimensional Polish standard-Borel space, with continuous/measurable finite restrictions:

• InfiniteGraph — a type synonym for SimpleGraph ℕ carrying the edge-coordinate (product) topology, via the coordinate equivalence InfiniteGraph.coordEquiv : InfiniteGraph ≃ (InfiniteGraph.EdgeIndex → Bool) (a simple graph on ℕ is exactly an arbitrary Bool assignment on off-diagonal unordered pairs);
• instances: CompactSpace, T2Space, MetrizableSpace, PolishSpace, MeasurableSpace (Borel), BorelSpace, StandardBorelSpace;
• InfiniteGraph.restrictFin k — restriction to the first k vertices (continuous, measurable);
• InfiniteGraph.padFin — embedding of a finite graph on Fin k (measurable), with restrictFin_padFin;
• InfiniteGraph.ext_of_map_restrictFin — finite-restriction measure extensionality: two finite Borel measures with equal pushforwards under every restrictFin k are equal (the restriction fibers form a generating π-system).

This is the infrastructure brick for the infinite exchangeable graph law (bricks A2–A3): the specialized Kolmogorov extension will be proved from compactness of ProbabilityMeasure InfiniteGraph plus this extensionality, with no general projective-limit machinery.

def InfiniteGraph : Type

Simple graphs on ℕ, as a type synonym carrying the edge-coordinate topology and its Borel structure.

Equations

• InfiniteGraph = SimpleGraph ℕ

@[reducible, inline]

abbrev InfiniteGraph.EdgeIndex : Type

The edge-coordinate index: off-diagonal unordered pairs of naturals.

Equations

• InfiniteGraph.EdgeIndex = { s : Sym2 ℕ // ¬s.IsDiag }

noncomputable def InfiniteGraph.coordEquiv : InfiniteGraph ≃ (EdgeIndex → Bool)

The coordinate equivalence: a simple graph on ℕ is exactly an arbitrary Bool assignment on off-diagonal unordered pairs.

Equations

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

@[implicit_reducible]

noncomputable instance InfiniteGraph.instTopologicalSpace : TopologicalSpace InfiniteGraph

Equations

• InfiniteGraph.instTopologicalSpace = TopologicalSpace.induced (⇑InfiniteGraph.coordEquiv) inferInstance

noncomputable def InfiniteGraph.coordHomeomorph : InfiniteGraph ≃ₜ (EdgeIndex → Bool)

The coordinate equivalence as a homeomorphism onto the full Boolean product.

Equations

• InfiniteGraph.coordHomeomorph = InfiniteGraph.coordEquiv.toHomeomorphOfIsInducing InfiniteGraph.coordHomeomorph._proof_1

instance InfiniteGraph.instCompactSpace : CompactSpace InfiniteGraph

instance InfiniteGraph.instT2Space : T2Space InfiniteGraph

instance InfiniteGraph.instSecondCountableTopology : SecondCountableTopology InfiniteGraph

instance InfiniteGraph.instMetrizableSpace : TopologicalSpace.MetrizableSpace InfiniteGraph

instance InfiniteGraph.instPolishSpaceForallEdgeIndexBool : PolishSpace (EdgeIndex → Bool)

instance InfiniteGraph.instPolishSpace : PolishSpace InfiniteGraph

@[implicit_reducible]

noncomputable instance InfiniteGraph.instMeasurableSpace : MeasurableSpace InfiniteGraph

Equations

• InfiniteGraph.instMeasurableSpace = borel InfiniteGraph

instance InfiniteGraph.instBorelSpace : BorelSpace InfiniteGraph

instance InfiniteGraph.instStandardBorelSpace : StandardBorelSpace InfiniteGraph

instance InfiniteGraph.instNonempty : Nonempty InfiniteGraph

Finite restriction and padding

def InfiniteGraph.restrictFin (k : ℕ) (G : InfiniteGraph) : SimpleGraph (Fin k)

Restriction to the first k vertices.

Equations

• InfiniteGraph.restrictFin k G = SimpleGraph.comap Fin.val G

def InfiniteGraph.padFin {k : ℕ} (H : SimpleGraph (Fin k)) : InfiniteGraph

Padding: a finite graph on Fin k, viewed as an infinite graph with no edges beyond the first k vertices.

Equations

• InfiniteGraph.padFin H = SimpleGraph.map (⇑Fin.valEmbedding) H

@[simp]

theorem InfiniteGraph.restrictFin_padFin {k : ℕ} (H : SimpleGraph (Fin k)) : restrictFin k (padFin H) = H

theorem InfiniteGraph.restrictFin_comap {k l : ℕ} (h : k ≤ l) (G : InfiniteGraph) : SimpleGraph.comap (⇑(Fin.castLEEmb h)) (restrictFin l G) = restrictFin k G

Restrictions are consistent under the initial-segment inclusions.

@[implicit_reducible]

instance InfiniteGraph.instTopologicalSpaceSimpleGraphFin (k : ℕ) : TopologicalSpace (SimpleGraph (Fin k))

Finite graph types carry the discrete topology (for the continuity statements about finite restrictions).

Equations

• InfiniteGraph.instTopologicalSpaceSimpleGraphFin k = ⊥

instance InfiniteGraph.instDiscreteTopologySimpleGraphFin (k : ℕ) : DiscreteTopology (SimpleGraph (Fin k))

instance InfiniteGraph.instMeasurableSingletonClassSimpleGraphFin (k : ℕ) : MeasurableSingletonClass (SimpleGraph (Fin k))

Singletons of finite graphs are measurable (Mathlib supplies the measurable space in Mathlib.MeasureTheory.Constructions.SimpleGraph but not this instance; also provided for countable V in Graphon/SamplingLaw.lean — this is the same Prop-valued fact, safe to duplicate).

instance InfiniteGraph.instOpensMeasurableSpaceSimpleGraphFin (k : ℕ) : OpensMeasurableSpace (SimpleGraph (Fin k))

Every open set of the (discrete) finite graph type is measurable.

@[simp]

theorem InfiniteGraph.coordEquiv_apply (G : InfiniteGraph) (e : EdgeIndex) : coordEquiv G e = if ↑e ∈ SimpleGraph.edgeSet G then true else false

The coordinate evaluation, unfolded.

theorem InfiniteGraph.continuous_restrictFin (k : ℕ) : Continuous (restrictFin k)

The restriction maps are continuous (the target is finite discrete; each fiber is a finite-coordinate cylinder).

theorem InfiniteGraph.measurable_restrictFin (k : ℕ) : Measurable (restrictFin k)

theorem InfiniteGraph.measurable_padFin {k : ℕ} : Measurable padFin

Finite-restriction measure extensionality

def InfiniteGraph.cylinders : Set (Set InfiniteGraph)

The finite-restriction cylinders: preimages of arbitrary finite-level sets.

Equations

• InfiniteGraph.cylinders = ⋃ (k : ℕ), Set.range fun (S : Set (SimpleGraph (Fin k))) => InfiniteGraph.restrictFin k ⁻¹' S

theorem InfiniteGraph.restrictFin_preimage_comap {k l : ℕ} (h : k ≤ l) (S : Set (SimpleGraph (Fin k))) : restrictFin k ⁻¹' S = restrictFin l ⁻¹' (fun (H : SimpleGraph (Fin l)) => SimpleGraph.comap (⇑(Fin.castLEEmb h)) H) ⁻¹' S

Lower-level cylinders are higher-level cylinders.

theorem InfiniteGraph.isPiSystem_cylinders : IsPiSystem cylinders

The cylinders form a π-system (align two levels at their maximum).

theorem InfiniteGraph.generateFrom_cylinders_eq : MeasurableSpace.generateFrom cylinders = inferInstance

The cylinders generate the Borel σ-algebra of the infinite graph space.

theorem InfiniteGraph.ext_of_map_restrictFin {μ ν : MeasureTheory.Measure InfiniteGraph} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (k : ℕ), MeasureTheory.Measure.map (restrictFin k) μ = MeasureTheory.Measure.map (restrictFin k) ν) : μ = ν

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

theorem InfiniteGraph.probabilityMeasure_ext_of_map_restrictFin {P Q : MeasureTheory.ProbabilityMeasure InfiniteGraph} (h : ∀ (k : ℕ), MeasureTheory.Measure.map (restrictFin k) ↑P = MeasureTheory.Measure.map (restrictFin k) ↑Q) : P = Q

Probability-measure form of the finite-restriction extensionality.