The finite sample law of a graphon (S2)

Bundles the sampled-graph masses sampleMass (Graphon/Sampling.lean) into a finite probability law and develops its algebraic API (issues #20 and #22; route vetted 2026-07-10):

• Graphon.upperSum / Graphon.upperSum_injective — the finite zeta/upper transform on SimpleGraph (Fin k) and its injectivity via Möbius inversion (IncidenceAlgebra.moebius_inversion_top). Together with the forward identity homDensity_eq_sum_sampleMass, this is the engine for every consistency statement below: two mass functions agree as soon as their supergraph sums agree.
• SimpleGraph.relabelOrderIso — relabeling by a permutation as an order isomorphism.
• Graphon.sampleMass_map_perm — relabeling invariance of the sample mass, proved by the upper-sum route (the direct inclusion–exclusion proof hits edgeFinset decidability-instance diamonds and is deliberately avoided).

This file deliberately lives above Graphon/Sampling.lean so that the incidence-algebra and PMF imports stay out of the foundational sampling module.

SimpleGraph relabeling plumbing (Mathlib candidates)

def SimpleGraph.relabelOrderIso {V : Type u_2} (σ : Equiv.Perm V) : SimpleGraph V ≃o SimpleGraph V

Relabeling the vertices of simple graphs by a permutation, as an order isomorphism of the subgraph lattice.

Equations

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

The upper transform and its injectivity

noncomputable def Graphon.upperSum {k : ℕ} (p : SimpleGraph (Fin k) → ℝ) (F : SimpleGraph (Fin k)) : ℝ

The finite zeta/upper transform of a mass function on SimpleGraph (Fin k): the total mass of the supergraphs of F. By homDensity_eq_sum_sampleMass, the upper transform of sampleMass W is homDensity · W.

Equations

• Graphon.upperSum p F = ∑ G : SimpleGraph (Fin k), if F ≤ G then p G else 0

theorem Graphon.upperSum_injective {k : ℕ} {p q : SimpleGraph (Fin k) → ℝ} (h : ∀ (F : SimpleGraph (Fin k)), upperSum p F = upperSum q F) : p = q

Injectivity of the upper transform (Möbius inversion over the finite subgraph lattice): a mass function on SimpleGraph (Fin k) is determined by its supergraph sums.

Relabeling invariance of the sample mass

theorem Graphon.upperSum_sampleMass {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {k : ℕ} (W : Graphon α μ) (F : SimpleGraph (Fin k)) [DecidableRel F.Adj] : upperSum W.sampleMass F = homDensity F W

The upper transform of the sample mass is the homomorphism density: the forward Möbius identity, restated through upperSum. Accepts an ambient [DecidableRel F.Adj] (bridged to the classical core by homDensity_congr_decRel).

theorem Graphon.sampleMass_map_perm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {k : ℕ} (W : Graphon α μ) (σ : Equiv.Perm (Fin k)) (G : SimpleGraph (Fin k)) : W.sampleMass (SimpleGraph.map (⇑(Equiv.toEmbedding σ)) G) = W.sampleMass G

Relabeling invariance of the sample mass: the law of the W-random graph is invariant under vertex permutations. Proved by the upper-sum route: the upper transform of the relabeled mass reindexes along SimpleGraph.relabelOrderIso σ to homDensity (F.map σ) W, which is homDensity F W by homDensity_map_embedding; upperSum_injective finishes.

Measurable-space plumbing for simple graphs (Mathlib candidates)

instance SimpleGraph.instMeasurableSingletonClassOfCountable_graphon {V : Type u_2} [Countable V] : MeasurableSingletonClass (SimpleGraph V)

The canonical measurable space on SimpleGraph V is discrete for countable V: singletons are measurable. (Mathlib supplies the measurable space in Mathlib.MeasureTheory.Constructions.SimpleGraph but not this instance.)

theorem SimpleGraph.measurable_comap {V : Type u_2} {W : Type u_3} (f : V → W) : Measurable fun (G : SimpleGraph W) => SimpleGraph.comap f G

theorem SimpleGraph.measurable_map_equiv {V : Type u_2} {W : Type u_3} (e : V ≃ W) : Measurable fun (G : SimpleGraph V) => SimpleGraph.map (⇑e.toEmbedding) G

The bundled sample law

noncomputable def Graphon.samplePMF {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (k : ℕ) : PMF (SimpleGraph (Fin k))

The finite sample law of a graphon, as a PMF: the distribution of the W-random graph G(k, W) on SimpleGraph (Fin k) (PMF.ofFintype over sampleMass; the masses are nonnegative and sum to one). The PMF is the finite algebraic API; sampleLaw below is its thin measurable wrapper.

Equations

• W.samplePMF k = PMF.ofFintype (fun (G : SimpleGraph (Fin k)) => ENNReal.ofReal (W.sampleMass G)) ⋯

@[simp]

theorem Graphon.samplePMF_apply {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (k : ℕ) (G : SimpleGraph (Fin k)) : (W.samplePMF k) G = ENNReal.ofReal (W.sampleMass G)

@[simp]

theorem Graphon.samplePMF_apply_toReal {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (k : ℕ) (G : SimpleGraph (Fin k)) : ((W.samplePMF k) G).toReal = W.sampleMass G

Point mass of the sample PMF as a real number. Composed with sampleMass_eq_sum_homDensity (Graphon/Sampling.lean), this IS the reverse Möbius/inclusion–exclusion identity at the PMF level — the intended API for expanding PMF point masses into signed homomorphism densities (#22).

noncomputable def Graphon.sampleLaw {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (k : ℕ) : MeasureTheory.ProbabilityMeasure (SimpleGraph (Fin k))

The finite sample law of a graphon, as a probability measure on the canonical measurable space of SimpleGraph (Fin k).

Equations

• W.sampleLaw k = ⟨(W.samplePMF k).toMeasure, ⋯⟩

@[simp]

theorem Graphon.sampleLaw_singleton {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (k : ℕ) (G : SimpleGraph (Fin k)) : ↑(W.sampleLaw k) {G} = ENNReal.ofReal (W.sampleMass G)

@[simp]

theorem Graphon.sampleLaw_singleton_toReal {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (k : ℕ) (G : SimpleGraph (Fin k)) : (↑(W.sampleLaw k) {G}).toReal = W.sampleMass G

Relabeling and arbitrary-injection consistency of the sample law

theorem Graphon.pmf_ext_of_upperSum {k : ℕ} {p q : PMF (SimpleGraph (Fin k))} (h : ∀ (F : SimpleGraph (Fin k)), upperSum (fun (G : SimpleGraph (Fin k)) => (p G).toReal) F = upperSum (fun (G : SimpleGraph (Fin k)) => (q G).toReal) F) : p = q

PMF extensionality through the upper transform: two PMFs on SimpleGraph (Fin k) agree as soon as all their supergraph masses agree.

theorem Graphon.upperSum_samplePMF {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {k : ℕ} (W : Graphon α μ) (F : SimpleGraph (Fin k)) [DecidableRel F.Adj] : upperSum (fun (G : SimpleGraph (Fin k)) => ((W.samplePMF k) G).toReal) F = homDensity F W

The upper mass of the sample PMF is the homomorphism density. Accepts an ambient [DecidableRel F.Adj].

theorem Graphon.samplePMF_map_comap {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {k l : ℕ} (W : Graphon α μ) (e : Fin k ↪ Fin l) : PMF.map (fun (H : SimpleGraph (Fin l)) => SimpleGraph.comap (⇑e) H) (W.samplePMF l) = W.samplePMF k

Arbitrary-injection consistency of the sample law: restricting the l-vertex W-random graph along any injection Fin k ↪ Fin l yields the k-vertex W-random graph. (Prefix restriction and relabeling-compatible restrictions are special cases.) Proof: upper masses of both sides are homDensity F W, via the Galois connection map_le_iff_le_comap and homDensity_map_embedding; upperSum_injective finishes.

theorem Graphon.samplePMF_map_relabel {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {k : ℕ} (W : Graphon α μ) (σ : Equiv.Perm (Fin k)) : PMF.map (fun (G : SimpleGraph (Fin k)) => SimpleGraph.map (⇑(Equiv.toEmbedding σ)) G) (W.samplePMF k) = W.samplePMF k

Relabeling invariance of the sample law (PMF form).

theorem Graphon.sampleLaw_map_comap {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {k l : ℕ} (W : Graphon α μ) (e : Fin k ↪ Fin l) : MeasureTheory.Measure.map (fun (H : SimpleGraph (Fin l)) => SimpleGraph.comap (⇑e) H) ↑(W.sampleLaw l) = ↑(W.sampleLaw k)

Arbitrary-injection consistency, measure form.

theorem Graphon.sampleLaw_map_relabel {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {k : ℕ} (W : Graphon α μ) (σ : Equiv.Perm (Fin k)) : MeasureTheory.Measure.map (fun (G : SimpleGraph (Fin k)) => SimpleGraph.map (⇑(Equiv.toEmbedding σ)) G) ↑(W.sampleLaw k) = ↑(W.sampleLaw k)

Relabeling invariance, measure form.