Continuous finite-law coordinates on the graphon space (issue #32)

The finite sample laws descend to point-separating continuous coordinates on the compact graphon space, giving a compact coordinate embedding into the product of finite mass-function spaces — the Lovász-style bridge toward exchangeable infinite graph laws:

• Graphon.lipschitzWith_homDensity / Graphon.continuous_homDensity — each homomorphism density is e(F)-Lipschitz in cut distance (the counting lemma homDensity_sub_le_of_cutDistance), hence continuous on raw graphons;
• Graphon.continuous_sampleMass — each singleton sample mass is a finite signed combination of homomorphism densities (sampleMass_eq_sum_homDensity), hence continuous;
• GraphonSpace.finiteSampleLaw — the k-vertex sample law descends through the quotient (well-defined by the joining theorem);
• GraphonSpace.finiteSampleLaw_eq_all_iff — the coordinates separate points;
• GraphonSpace.isClosedEmbedding_sampleCoordinates — the combined coordinates are a closed embedding of the compact graphon space into Π k, SimpleGraph (Fin k) → ℝ.

(PMF carries no topology in Mathlib, so continuity statements are coordinatewise via toReal masses, and the embedding lands in real-valued mass functions.)

theorem Graphon.dist_eq_cutDistance {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (U W : Graphon α μ) : dist U W = U.cutDistance W

dist on raw graphons is the cut distance (definitional unfolding of Graphon.instPseudoMetricSpace).

theorem Graphon.lipschitzWith_homDensity {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] : LipschitzWith ↑F.edgeFinset.card fun (W : Graphon α μ) => homDensity F W

Each homomorphism density is e(F)-Lipschitz in cut distance (counting lemma).

theorem Graphon.continuous_homDensity {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] : Continuous fun (W : Graphon α μ) => homDensity F W

Each homomorphism density is continuous on raw graphons.

theorem Graphon.continuous_sampleMass {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {k : ℕ} (G : SimpleGraph (Fin k)) : Continuous fun (W : Graphon α μ) => W.sampleMass G

Each singleton sample mass is continuous on raw graphons: it is a finite signed combination of homomorphism densities.

noncomputable def GraphonSpace.sampleMassCoord {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {k : ℕ} (G : SimpleGraph (Fin k)) : GraphonSpace α μ → ℝ

The scalar mass coordinate: the probability that the k-vertex sample of a graphon class equals G, as a real-valued function on the graphon space (sampleMass descends through the quotient, well-defined by the joining theorem).

Equations

• GraphonSpace.sampleMassCoord G = SeparationQuotient.lift (fun (W : Graphon α μ) => W.sampleMass G) ⋯

@[simp]

theorem GraphonSpace.sampleMassCoord_mk {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {k : ℕ} (G : SimpleGraph (Fin k)) (W : Graphon α μ) : sampleMassCoord G (mk W) = W.sampleMass G

theorem GraphonSpace.continuous_sampleMassCoord {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {k : ℕ} (G : SimpleGraph (Fin k)) : Continuous (sampleMassCoord G)

noncomputable def GraphonSpace.finiteSampleLaw {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (k : ℕ) : GraphonSpace α μ → PMF (SimpleGraph (Fin k))

The k-vertex sample law as a coordinate on the graphon space: samplePMF descends through the quotient (well-defined by the joining theorem). The scalar sampleMassCoord is its toReal mass; downstream topology uses the scalar form (Mathlib gives PMF no topology).

Equations

• GraphonSpace.finiteSampleLaw k = SeparationQuotient.lift (fun (W : Graphon α μ) => W.samplePMF k) ⋯

@[simp]

theorem GraphonSpace.finiteSampleLaw_mk {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (k : ℕ) (W : Graphon α μ) : finiteSampleLaw k (mk W) = W.samplePMF k

theorem GraphonSpace.sampleMassCoord_eq_toReal {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {k : ℕ} (G : SimpleGraph (Fin k)) (x : GraphonSpace α μ) : sampleMassCoord G x = ((finiteSampleLaw k x) G).toReal

The scalar coordinate is the toReal mass of the descended sample law.

theorem GraphonSpace.finiteSampleLaw_eq_all_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {x y : GraphonSpace α μ} : (∀ (k : ℕ), finiteSampleLaw k x = finiteSampleLaw k y) ↔ x = y

The sample-law coordinates separate points of the graphon space.

theorem GraphonSpace.continuous_finiteSampleLaw_apply {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (k : ℕ) (G : SimpleGraph (Fin k)) : Continuous fun (x : GraphonSpace α μ) => ((finiteSampleLaw k x) G).toReal

Each mass coordinate of each finite sample law is continuous on the graphon space.

noncomputable def GraphonSpace.sampleCoordinates {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (x : GraphonSpace α μ) (k : ℕ) : SimpleGraph (Fin k) → ℝ

The combined sample-law coordinates, into the product of finite real-valued mass-function spaces.

Equations

• x.sampleCoordinates x✝ G = GraphonSpace.sampleMassCoord G x

@[simp]

theorem GraphonSpace.sampleCoordinates_apply {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (x : GraphonSpace α μ) (k : ℕ) (G : SimpleGraph (Fin k)) : x.sampleCoordinates k G = sampleMassCoord G x

theorem GraphonSpace.continuous_sampleCoordinates {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : Continuous sampleCoordinates

theorem GraphonSpace.injective_sampleCoordinates {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : Function.Injective sampleCoordinates

theorem GraphonSpace.isClosedEmbedding_sampleCoordinates {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : Topology.IsClosedEmbedding sampleCoordinates

Compact coordinate embedding (Lovász-style): the sample-law coordinates embed the compact graphon space homeomorphically onto a closed subset of the product of finite mass-function spaces — a continuous injection from a compact space into a Hausdorff space.

The image lies in the consistent finite probability simplices

theorem GraphonSpace.sampleMassCoord_nonneg {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {k : ℕ} (G : SimpleGraph (Fin k)) (x : GraphonSpace α μ) : 0 ≤ sampleMassCoord G x

theorem GraphonSpace.sum_sampleMassCoord {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (k : ℕ) (x : GraphonSpace α μ) : ∑ G : SimpleGraph (Fin k), sampleMassCoord G x = 1

theorem GraphonSpace.finiteSampleLaw_map_comap {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {k l : ℕ} (e : Fin k ↪ Fin l) (x : GraphonSpace α μ) : PMF.map (fun (G : SimpleGraph (Fin l)) => SimpleGraph.comap (⇑e) G) (finiteSampleLaw l x) = finiteSampleLaw k x

Injection consistency of the sample-law coordinates (descends samplePMF_map_comap through the quotient).

theorem GraphonSpace.sum_sampleMassCoord_comap {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {k l : ℕ} (e : Fin k ↪ Fin l) (G : SimpleGraph (Fin k)) (x : GraphonSpace α μ) : (∑ H : SimpleGraph (Fin l), if G = SimpleGraph.comap (⇑e) H then sampleMassCoord H x else 0) = sampleMassCoord G x

Scalar form of injection consistency: the coordinates satisfy the marginal equations of a consistent family.