The sample laws determine the graphon (S2–S3 joining theorem)

Two graphons have the same finite sample laws at every size iff they are weakly isomorphic — equivalently, iff they define the same point of the graphon space:

• Graphon.samplePMF_eq_all_iff_weaklyIsomorphic — sample laws ↔ weak isomorphism. Forward: equal laws have equal upper masses, which are the homomorphism densities (upperSum_samplePMF), and densities determine the graphon (weaklyIsomorphic_of_homDensity_eq, the inverse-counting headline). Reverse: cut distance zero forces equal densities (homDensity_eq_of_cutDistance_zero, the counting lemma), hence equal upper masses, hence equal PMFs (pmf_ext_of_upperSum).
• Graphon.samplePMF_eq_all_iff_mk_eq_mk — the quotient-facing form: same sample laws iff the same point of GraphonSpace.

This joins the S2 finite-marginal API to the S3 state space: the maps GraphonSpace.mk W ↦ samplePMF W k are well-defined coordinates on the graphon space that separate points — the Lovász-style bridge toward exchangeable infinite graph laws.

This file sits above both SamplingLaw and InverseCounting so that the foundational sample-law module does not import the inverse-counting machinery.

theorem Graphon.samplePMF_eq_all_iff_weaklyIsomorphic {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (U W : Graphon α μ) : (∀ (k : ℕ), U.samplePMF k = W.samplePMF k) ↔ U.WeaklyIsomorphic W

The sample laws determine the graphon: two graphons have the same k-vertex sample law for every k iff they are weakly isomorphic.

theorem Graphon.samplePMF_eq_all_iff_mk_eq_mk {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (U W : Graphon α μ) : (∀ (k : ℕ), U.samplePMF k = W.samplePMF k) ↔ GraphonSpace.mk U = GraphonSpace.mk W

The quotient-facing form: two graphons have the same sample laws iff they define the same point of the graphon space. The maps mk W ↦ samplePMF W k are therefore point-separating coordinates on GraphonSpace.